Theorem superpos 10306

Description: Superposition Principle. If A and B are distinct atoms, there exists a third atom, distinct from A and B, that is the superposition of A and B. Definition 3.4-3(a) in [MegillPavicic] p. 2345 (PDF p. 8).

Assertion

Ref	Expression
superpos	⊢ ((A ∈ Atoms ⋀ B ∈ Atoms ⋀ A ≠ B) → ∃x ∈ Atoms (x ≠ A ⋀ x ≠ B ⋀ x ⊆ (A ∨ℋ B)))

Distinct variable groups:   x,A   x,B

Proof of Theorem superpos

Step	Hyp	Ref	Expression
1		reeanv 1785	. . . 4 ⊢ (∃y ∈ ℋ ∃z ∈ ℋ ((y ≠ 0h ⋀ A = (span ‘{y})) ⋀ (z ≠ 0h ⋀ B = (span ‘{z}))) ↔ (∃y ∈ ℋ (y ≠ 0h ⋀ A = (span ‘{y})) ⋀ ∃z ∈ ℋ (z ≠ 0h ⋀ B = (span ‘{z}))))
2		neeq1 1597	. . . . . . . . . . 11 ⊢ (A = (span ‘{y}) → (A ≠ B ↔ (span ‘{y}) ≠ B))
3		neeq2 1598	. . . . . . . . . . 11 ⊢ (B = (span ‘{z}) → ((span ‘{y}) ≠ B ↔ (span ‘{y}) ≠ (span ‘{z})))
4	2, 3	sylan9bb 543	. . . . . . . . . 10 ⊢ ((A = (span ‘{y}) ⋀ B = (span ‘{z})) → (A ≠ B ↔ (span ‘{y}) ≠ (span ‘{z})))
5	4	adantl 390	. . . . . . . . 9 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) → (A ≠ B ↔ (span ‘{y}) ≠ (span ‘{z})))
6		neeq1 1597	. . . . . . . . . . . . 13 ⊢ (x = (span ‘{(y +h z)}) → (x ≠ A ↔ (span ‘{(y +h z)}) ≠ A))
7		neeq1 1597	. . . . . . . . . . . . 13 ⊢ (x = (span ‘{(y +h z)}) → (x ≠ B ↔ (span ‘{(y +h z)}) ≠ B))
8		sseq1 2093	. . . . . . . . . . . . 13 ⊢ (x = (span ‘{(y +h z)}) → (x ⊆ (A ∨ℋ B) ↔ (span ‘{(y +h z)}) ⊆ (A ∨ℋ B)))
9	6, 7, 8	3anbi123d 897	. . . . . . . . . . . 12 ⊢ (x = (span ‘{(y +h z)}) → ((x ≠ A ⋀ x ≠ B ⋀ x ⊆ (A ∨ℋ B)) ↔ ((span ‘{(y +h z)}) ≠ A ⋀ (span ‘{(y +h z)}) ≠ B ⋀ (span ‘{(y +h z)}) ⊆ (A ∨ℋ B))))
10	9	rcla4ev 1884	. . . . . . . . . . 11 ⊢ (((span ‘{(y +h z)}) ∈ Atoms ⋀ ((span ‘{(y +h z)}) ≠ A ⋀ (span ‘{(y +h z)}) ≠ B ⋀ (span ‘{(y +h z)}) ⊆ (A ∨ℋ B))) → ∃x ∈ Atoms (x ≠ A ⋀ x ≠ B ⋀ x ⊆ (A ∨ℋ B)))
11		spansna 10302	. . . . . . . . . . . . . 14 ⊢ (((y +h z) ∈ ℋ ⋀ (y +h z) ≠ 0h) → (span ‘{(y +h z)}) ∈ Atoms)
12		hvaddcl 8906	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (y +h z) ∈ ℋ )
13	12	adantr 391	. . . . . . . . . . . . . 14 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (y +h z) ∈ ℋ )
14		hvaddeq0 8960	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((y +h z) = 0h ↔ y = (-1 ·h z)))
15		sneq 2429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = (-1 ·h z) → {y} = {(-1 ·h z)})
16	15	fveq2d 3744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = (-1 ·h z) → (span ‘{y}) = (span ‘{(-1 ·h z)}))
17		ax1cn 5289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
18	17	negcli 5389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 ∈ ℂ
19		ax1ne0 5300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
20	17, 19	negn0i 5820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 ≠ 0
21		spansncol 9515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ ℋ ⋀ -1 ∈ ℂ ⋀ -1 ≠ 0) → (span ‘{(-1 ·h z)}) = (span ‘{z}))
22	18, 20, 21	mp3an23 912	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z ∈ ℋ → (span ‘{(-1 ·h z)}) = (span ‘{z}))
23	16, 22	sylan9eqr 1536	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ ℋ ⋀ y = (-1 ·h z)) → (span ‘{y}) = (span ‘{z}))
24	23	ex 373	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ ℋ → (y = (-1 ·h z) → (span ‘{y}) = (span ‘{z})))
25	24	adantl 390	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (y = (-1 ·h z) → (span ‘{y}) = (span ‘{z})))
26	14, 25	sylbid 203	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((y +h z) = 0h → (span ‘{y}) = (span ‘{z})))
27	26	necon3d 1611	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{y}) ≠ (span ‘{z}) → (y +h z) ≠ 0h))
28	27	imp 350	. . . . . . . . . . . . . 14 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (y +h z) ≠ 0h)
29	11, 13, 28	sylanc 474	. . . . . . . . . . . . 13 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (span ‘{(y +h z)}) ∈ Atoms)
30	29	adantlr 395	. . . . . . . . . . . 12 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (span ‘{(y +h z)}) ∈ Atoms)
31	30	adantlr 395	. . . . . . . . . . 11 ⊢ (((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (span ‘{(y +h z)}) ∈ Atoms)
32		eqeq2 1491	. . . . . . . . . . . . . . . . . 18 ⊢ (A = (span ‘{y}) → ((span ‘{(y +h z)}) = A ↔ (span ‘{(y +h z)}) = (span ‘{y})))
33	32	biimpd 153	. . . . . . . . . . . . . . . . 17 ⊢ (A = (span ‘{y}) → ((span ‘{(y +h z)}) = A → (span ‘{(y +h z)}) = (span ‘{y})))
34		spansneleqi 9516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y +h z) ∈ ℋ → ((span ‘{(y +h z)}) = (span ‘{y}) → (y +h z) ∈ (span ‘{y})))
35	12, 34	syl 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{(y +h z)}) = (span ‘{y}) → (y +h z) ∈ (span ‘{y})))
36		elspansn 9513	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ∈ ℋ → ((y +h z) ∈ (span ‘{y}) ↔ ∃v ∈ ℂ (y +h z) = (v ·h y)))
37	36	adantr 391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((y +h z) ∈ (span ‘{y}) ↔ ∃v ∈ ℂ (y +h z) = (v ·h y)))
38		opreq1 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w = (v + -1) → (w ·h y) = ((v + -1) ·h y))
39	38	eqeq2d 1493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = (v + -1) → (z = (w ·h y) ↔ z = ((v + -1) ·h y)))
40	39	rcla4ev 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((v + -1) ∈ ℂ ⋀ z = ((v + -1) ·h y)) → ∃w ∈ ℂ z = (w ·h y))
41		addcl 5321	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((v ∈ ℂ ⋀ -1 ∈ ℂ) → (v + -1) ∈ ℂ)
42	18, 41	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v ∈ ℂ → (v + -1) ∈ ℂ)
43	42	ad2antlr 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h y)) → (v + -1) ∈ ℂ)
44		hvsubadd 8968	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((v ·h y) ∈ ℋ ⋀ y ∈ ℋ ⋀ z ∈ ℋ ) → (((v ·h y) −h y) = z ↔ (y +h z) = (v ·h y)))
45		hvmulcl 8907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v ∈ ℂ ⋀ y ∈ ℋ ) → (v ·h y) ∈ ℋ )
46	45	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((y ∈ ℋ ⋀ v ∈ ℂ) → (v ·h y) ∈ ℋ )
47	46	adantlr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → (v ·h y) ∈ ℋ )
48		simpll 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → y ∈ ℋ )
49		simplr 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → z ∈ ℋ )
50	44, 47, 48, 49	syl3anc 862	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → (((v ·h y) −h y) = z ↔ (y +h z) = (v ·h y)))
51	50	biimpar 419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h y)) → ((v ·h y) −h y) = z)
52		hvsubval 8910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((v ·h y) ∈ ℋ ⋀ y ∈ ℋ ) → ((v ·h y) −h y) = ((v ·h y) +h (-1 ·h y)))
53	45, 52	sylancom 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v ∈ ℂ ⋀ y ∈ ℋ ) → ((v ·h y) −h y) = ((v ·h y) +h (-1 ·h y)))
54		ax-hvdistr2 8903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((v ∈ ℂ ⋀ -1 ∈ ℂ ⋀ y ∈ ℋ ) → ((v + -1) ·h y) = ((v ·h y) +h (-1 ·h y)))
55	18, 54	mp3an2 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v ∈ ℂ ⋀ y ∈ ℋ ) → ((v + -1) ·h y) = ((v ·h y) +h (-1 ·h y)))
56	53, 55	eqtr4d 1517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((v ∈ ℂ ⋀ y ∈ ℋ ) → ((v ·h y) −h y) = ((v + -1) ·h y))
57	56	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((y ∈ ℋ ⋀ v ∈ ℂ) → ((v ·h y) −h y) = ((v + -1) ·h y))
58	57	adantlr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → ((v ·h y) −h y) = ((v + -1) ·h y))
59	58	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h y)) → ((v ·h y) −h y) = ((v + -1) ·h y))
60	51, 59	eqtr3d 1516	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h y)) → z = ((v + -1) ·h y))
61	40, 43, 60	sylanc 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h y)) → ∃w ∈ ℂ z = (w ·h y))
62	61	exp31 378	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (v ∈ ℂ → ((y +h z) = (v ·h y) → ∃w ∈ ℂ z = (w ·h y))))
63	62	r19.23adv 1753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (∃v ∈ ℂ (y +h z) = (v ·h y) → ∃w ∈ ℂ z = (w ·h y)))
64	37, 63	sylbid 203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((y +h z) ∈ (span ‘{y}) → ∃w ∈ ℂ z = (w ·h y)))
65	35, 64	syld 27	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{(y +h z)}) = (span ‘{y}) → ∃w ∈ ℂ z = (w ·h y)))
66		elspansn 9513	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ ℋ → (z ∈ (span ‘{y}) ↔ ∃w ∈ ℂ z = (w ·h y)))
67	66	adantr 391	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (z ∈ (span ‘{y}) ↔ ∃w ∈ ℂ z = (w ·h y)))
68	65, 67	sylibrd 204	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{(y +h z)}) = (span ‘{y}) → z ∈ (span ‘{y})))
69	68	adantr 391	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ z ≠ 0h) → ((span ‘{(y +h z)}) = (span ‘{y}) → z ∈ (span ‘{y})))
70		spansneleq 9517	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℋ ⋀ z ≠ 0h) → (z ∈ (span ‘{y}) → (span ‘{z}) = (span ‘{y})))
71		eqcom 1484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((span ‘{z}) = (span ‘{y}) ↔ (span ‘{y}) = (span ‘{z}))
72	70, 71	syl6ib 212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ ℋ ⋀ z ≠ 0h) → (z ∈ (span ‘{y}) → (span ‘{y}) = (span ‘{z})))
73	72	adantlr 395	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ z ≠ 0h) → (z ∈ (span ‘{y}) → (span ‘{y}) = (span ‘{z})))
74	69, 73	syld 27	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ z ≠ 0h) → ((span ‘{(y +h z)}) = (span ‘{y}) → (span ‘{y}) = (span ‘{z})))
75	33, 74	sylan9r 472	. . . . . . . . . . . . . . . 16 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ z ≠ 0h) ⋀ A = (span ‘{y})) → ((span ‘{(y +h z)}) = A → (span ‘{y}) = (span ‘{z})))
76	75	necon3d 1611	. . . . . . . . . . . . . . 15 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ z ≠ 0h) ⋀ A = (span ‘{y})) → ((span ‘{y}) ≠ (span ‘{z}) → (span ‘{(y +h z)}) ≠ A))
77	76	adantlrl 400	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ A = (span ‘{y})) → ((span ‘{y}) ≠ (span ‘{z}) → (span ‘{(y +h z)}) ≠ A))
78	77	adantrr 397	. . . . . . . . . . . . 13 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) → ((span ‘{y}) ≠ (span ‘{z}) → (span ‘{(y +h z)}) ≠ A))
79	78	imp 350	. . . . . . . . . . . 12 ⊢ (((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (span ‘{(y +h z)}) ≠ A)
80		eqeq2 1491	. . . . . . . . . . . . . . . . . 18 ⊢ (B = (span ‘{z}) → ((span ‘{(y +h z)}) = B ↔ (span ‘{(y +h z)}) = (span ‘{z})))
81	80	biimpd 153	. . . . . . . . . . . . . . . . 17 ⊢ (B = (span ‘{z}) → ((span ‘{(y +h z)}) = B → (span ‘{(y +h z)}) = (span ‘{z})))
82		spansneleqi 9516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y +h z) ∈ ℋ → ((span ‘{(y +h z)}) = (span ‘{z}) → (y +h z) ∈ (span ‘{z})))
83	12, 82	syl 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{(y +h z)}) = (span ‘{z}) → (y +h z) ∈ (span ‘{z})))
84		elspansn 9513	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ∈ ℋ → ((y +h z) ∈ (span ‘{z}) ↔ ∃v ∈ ℂ (y +h z) = (v ·h z)))
85	84	adantl 390	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((y +h z) ∈ (span ‘{z}) ↔ ∃v ∈ ℂ (y +h z) = (v ·h z)))
86		opreq1 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w = (v + -1) → (w ·h z) = ((v + -1) ·h z))
87	86	eqeq2d 1493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = (v + -1) → (y = (w ·h z) ↔ y = ((v + -1) ·h z)))
88	87	rcla4ev 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((v + -1) ∈ ℂ ⋀ y = ((v + -1) ·h z)) → ∃w ∈ ℂ y = (w ·h z))
89	42	ad2antlr 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h z)) → (v + -1) ∈ ℂ)
90		hvsubadd 8968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((v ·h z) ∈ ℋ ⋀ z ∈ ℋ ⋀ y ∈ ℋ ) → (((v ·h z) −h z) = y ↔ (z +h y) = (v ·h z)))
91		hvmulcl 8907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((v ∈ ℂ ⋀ z ∈ ℋ ) → (v ·h z) ∈ ℋ )
92	91	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((z ∈ ℋ ⋀ v ∈ ℂ) → (v ·h z) ∈ ℋ )
93	92	adantll 394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → (v ·h z) ∈ ℋ )
94	90, 93, 49, 48	syl3anc 862	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → (((v ·h z) −h z) = y ↔ (z +h y) = (v ·h z)))
95		ax-hvcom 8895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (y +h z) = (z +h y))
96	95	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → (y +h z) = (z +h y))
97	96	eqeq1d 1490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → ((y +h z) = (v ·h z) ↔ (z +h y) = (v ·h z)))
98	94, 97	bitr4d 534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → (((v ·h z) −h z) = y ↔ (y +h z) = (v ·h z)))
99	98	biimpar 419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h z)) → ((v ·h z) −h z) = y)
100		hvsubval 8910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((v ·h z) ∈ ℋ ⋀ z ∈ ℋ ) → ((v ·h z) −h z) = ((v ·h z) +h (-1 ·h z)))
101	91, 100	sylancom 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v ∈ ℂ ⋀ z ∈ ℋ ) → ((v ·h z) −h z) = ((v ·h z) +h (-1 ·h z)))
102		ax-hvdistr2 8903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((v ∈ ℂ ⋀ -1 ∈ ℂ ⋀ z ∈ ℋ ) → ((v + -1) ·h z) = ((v ·h z) +h (-1 ·h z)))
103	18, 102	mp3an2 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v ∈ ℂ ⋀ z ∈ ℋ ) → ((v + -1) ·h z) = ((v ·h z) +h (-1 ·h z)))
104	101, 103	eqtr4d 1517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((v ∈ ℂ ⋀ z ∈ ℋ ) → ((v ·h z) −h z) = ((v + -1) ·h z))
105	104	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((z ∈ ℋ ⋀ v ∈ ℂ) → ((v ·h z) −h z) = ((v + -1) ·h z))
106	105	adantll 394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) → ((v ·h z) −h z) = ((v + -1) ·h z))
107	106	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h z)) → ((v ·h z) −h z) = ((v + -1) ·h z))
108	99, 107	eqtr3d 1516	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h z)) → y = ((v + -1) ·h z))
109	88, 89, 108	sylanc 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ v ∈ ℂ) ⋀ (y +h z) = (v ·h z)) → ∃w ∈ ℂ y = (w ·h z))
110	109	exp31 378	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (v ∈ ℂ → ((y +h z) = (v ·h z) → ∃w ∈ ℂ y = (w ·h z))))
111	110	r19.23adv 1753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (∃v ∈ ℂ (y +h z) = (v ·h z) → ∃w ∈ ℂ y = (w ·h z)))
112	85, 111	sylbid 203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((y +h z) ∈ (span ‘{z}) → ∃w ∈ ℂ y = (w ·h z)))
113	83, 112	syld 27	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{(y +h z)}) = (span ‘{z}) → ∃w ∈ ℂ y = (w ·h z)))
114		elspansn 9513	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z ∈ ℋ → (y ∈ (span ‘{z}) ↔ ∃w ∈ ℂ y = (w ·h z)))
115	114	adantl 390	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (y ∈ (span ‘{z}) ↔ ∃w ∈ ℂ y = (w ·h z)))
116	113, 115	sylibrd 204	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → ((span ‘{(y +h z)}) = (span ‘{z}) → y ∈ (span ‘{z})))
117	116	adantr 391	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ y ≠ 0h) → ((span ‘{(y +h z)}) = (span ‘{z}) → y ∈ (span ‘{z})))
118		spansneleq 9517	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ ℋ ⋀ y ≠ 0h) → (y ∈ (span ‘{z}) → (span ‘{y}) = (span ‘{z})))
119	118	adantll 394	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ y ≠ 0h) → (y ∈ (span ‘{z}) → (span ‘{y}) = (span ‘{z})))
120	117, 119	syld 27	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ y ≠ 0h) → ((span ‘{(y +h z)}) = (span ‘{z}) → (span ‘{y}) = (span ‘{z})))
121	81, 120	sylan9r 472	. . . . . . . . . . . . . . . 16 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ y ≠ 0h) ⋀ B = (span ‘{z})) → ((span ‘{(y +h z)}) = B → (span ‘{y}) = (span ‘{z})))
122	121	necon3d 1611	. . . . . . . . . . . . . . 15 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ y ≠ 0h) ⋀ B = (span ‘{z})) → ((span ‘{y}) ≠ (span ‘{z}) → (span ‘{(y +h z)}) ≠ B))
123	122	adantlrr 401	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ B = (span ‘{z})) → ((span ‘{y}) ≠ (span ‘{z}) → (span ‘{(y +h z)}) ≠ B))
124	123	adantrl 396	. . . . . . . . . . . . 13 ⊢ ((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) → ((span ‘{y}) ≠ (span ‘{z}) → (span ‘{(y +h z)}) ≠ B))
125	124	imp 350	. . . . . . . . . . . 12 ⊢ (((((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (y ≠ 0h ⋀ z ≠ 0h)) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) ⋀ (span ‘{y}) ≠ (span ‘{z})) → (span ‘{(y +h z)}) ≠ B)
126		spanpr 9527	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (span ‘{(y +h z)}) ⊆ (span ‘{y, z}))
127	126	adantr 391	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ ℋ ⋀ z ∈ ℋ ) ⋀ (A = (span ‘{y}) ⋀ B = (span ‘{z}))) → (span ‘{(y +h z)}) ⊆ (span ‘{y, z}))
128		opreq12 3986	. . . . . . . . . . . . . . . 16 ⊢ ((A = (span ‘{y}) ⋀ B = (span ‘{z})) → (A ∨ℋ B) = ((span ‘{y}) ∨ℋ (span ‘{z})))
129		spanun 9492	. . . . . . . . . . . . . . . . . . 19 ⊢ (({y} ⊆ ℋ ⋀ {z} ⊆ ℋ ) → (span ‘({y} ∪ {z})) = ((span ‘{y}) +ℋ (span ‘{z})))
130		snssi 2480	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ ℋ → {y} ⊆ ℋ )
131		snssi 2480	. . . . . . . . . . . . . . . . . . 19 ⊢ (z ∈ ℋ → {z} ⊆ ℋ )
132	129, 130, 131	syl2an 457	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ ℋ ⋀ z ∈ ℋ ) → (span ‘({y} ∪ {z})) = ((span ‘{y}) +ℋ (span ‘{z})))
133