Theorem superpos 10365

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 e. Atoms /\ B e. Atoms /\ A =/= B) -> E.x e. Atoms (x =/= A /\ x =/= B /\ x (_ (A vH B)))

Distinct variable groups:   x,A   x,B

Proof of Theorem superpos

Step	Hyp	Ref	Expression
1		reeanv 1825	. . . 4 |- (E.y e. H~ E.z e. H~ ((y =/= 0h /\ A = (span` {y})) /\ (z =/= 0h /\ B = (span` {z}))) <-> (E.y e. H~ (y =/= 0h /\ A = (span` {y})) /\ E.z e. H~ (z =/= 0h /\ B = (span` {z}))))
2		neeq1 1637	. . . . . . . . . . 11 |- (A = (span` {y}) -> (A =/= B <-> (span` {y}) =/= B))
3		neeq2 1638	. . . . . . . . . . 11 |- (B = (span` {z}) -> ((span` {y}) =/= B <-> (span` {y}) =/= (span` {z})))
4	2, 3	sylan9bb 551	. . . . . . . . . 10 |- ((A = (span` {y}) /\ B = (span` {z})) -> (A =/= B <-> (span` {y}) =/= (span` {z})))
5	4	adantl 397	. . . . . . . . 9 |- ((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (A = (span` {y}) /\ B = (span` {z}))) -> (A =/= B <-> (span` {y}) =/= (span` {z})))
6		neeq1 1637	. . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x =/= A <-> (span` {(y +h z)}) =/= A))
7		neeq1 1637	. . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x =/= B <-> (span` {(y +h z)}) =/= B))
8		sseq1 2133	. . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x (_ (A vH B) <-> (span` {(y +h z)}) (_ (A vH B)))
9	6, 7, 8	3anbi123d 905	. . . . . . . . . . . 12 |- (x = (span` {(y +h z)}) -> ((x =/= A /\ x =/= B /\ x (_ (A vH B)) <-> ((span` {(y +h z)}) =/= A /\ (span` {(y +h z)}) =/= B /\ (span` {(y +h z)}) (_ (A vH B))))
10	9	rcla4ev 1924	. . . . . . . . . . 11 |- (((span` {(y +h z)}) e. Atoms /\ ((span` {(y +h z)}) =/= A /\ (span` {(y +h z)}) =/= B /\ (span` {(y +h z)}) (_ (A vH B))) -> E.x e. Atoms (x =/= A /\ x =/= B /\ x (_ (A vH B)))
11		spansna 10361	. . . . . . . . . . . . . 14 |- (((y +h z) e. H~ /\ (y +h z) =/= 0h) -> (span` {(y +h z)}) e. Atoms)
12		hvaddcl 8965	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> (y +h z) e. H~)
13	12	adantr 398	. . . . . . . . . . . . . 14 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (y +h z) e. H~)
14		hvaddeq0 9019	. . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ z e. H~) -> ((y +h z) = 0h <-> y = (-u1 .h z)))
15		sneq 2469	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (-u1 .h z) -> {y} = {(-u1 .h z)})
16	15	fveq2d 3785	. . . . . . . . . . . . . . . . . . . 20 |- (y = (-u1 .h z) -> (span` {y}) = (span` {(-u1 .h z)}))
17		ax1cn 5334	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
18	17	negcli 5434	. . . . . . . . . . . . . . . . . . . . 21 |- -u1 e. CC
19		ax1ne0 5345	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 =/= 0
20	17, 19	negn0i 5866	. . . . . . . . . . . . . . . . . . . . 21 |- -u1 =/= 0
21		spansncol 9574	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. H~ /\ -u1 e. CC /\ -u1 =/= 0) -> (span` {(-u1 .h z)}) = (span` {z}))
22	18, 20, 21	mp3an23 920	. . . . . . . . . . . . . . . . . . . 20 |- (z e. H~ -> (span` {(-u1 .h z)}) = (span` {z}))
23	16, 22	sylan9eqr 1576	. . . . . . . . . . . . . . . . . . 19 |- ((z e. H~ /\ y = (-u1 .h z)) -> (span` {y}) = (span` {z}))
24	23	ex 380	. . . . . . . . . . . . . . . . . 18 |- (z e. H~ -> (y = (-u1 .h z) -> (span` {y}) = (span` {z})))
25	24	adantl 397	. . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ z e. H~) -> (y = (-u1 .h z) -> (span` {y}) = (span` {z})))
26	14, 25	sylbid 210	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ z e. H~) -> ((y +h z) = 0h -> (span` {y}) = (span` {z})))
27	26	necon3d 1651	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> ((span` {y}) =/= (span` {z}) -> (y +h z) =/= 0h))
28	27	imp 357	. . . . . . . . . . . . . 14 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (y +h z) =/= 0h)
29	11, 13, 28	sylanc 482	. . . . . . . . . . . . 13 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
30	29	adantlr 402	. . . . . . . . . . . 12 |- ((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
31	30	adantlr 402	. . . . . . . . . . 11 |- (((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (A = (span` {y}) /\ B = (span` {z}))) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
32		eqeq2 1531	. . . . . . . . . . . . . . . . . 18 |- (A = (span` {y}) -> ((span` {(y +h z)}) = A <-> (span` {(y +h z)}) = (span` {y})))
33	32	biimpd 160	. . . . . . . . . . . . . . . . 17 |- (A = (span` {y}) -> ((span` {(y +h z)}) = A -> (span` {(y +h z)}) = (span` {y})))
34		spansneleqi 9575	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y +h z) e. H~ -> ((span` {(y +h z)}) = (span` {y}) -> (y +h z) e. (span` {y})))
35	12, 34	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. H~ /\ z e. H~) -> ((span` {(y +h z)}) = (span` {y}) -> (y +h z) e. (span` {y})))
36		elspansn 9572	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. H~ -> ((y +h z) e. (span` {y}) <-> E.v e. CC (y +h z) = (v .h y)))
37	36	adantr 398	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. H~ /\ z e. H~) -> ((y +h z) e. (span` {y}) <-> E.v e. CC (y +h z) = (v .h y)))
38		opreq1 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = (v + -u1) -> (w .h y) = ((v + -u1) .h y))
39	38	eqeq2d 1533	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (v + -u1) -> (z = (w .h y) <-> z = ((v + -u1) .h y)))
40	39	rcla4ev 1924	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((v + -u1) e. CC /\ z = ((v + -u1) .h y)) -> E.w e. CC z = (w .h y))
41		addcl 5366	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((v e. CC /\ -u1 e. CC) -> (v + -u1) e. CC)
42	18, 41	mpan2 708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. CC -> (v + -u1) e. CC)
43	42	ad2antlr 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((y e. H~ /\ z e. H~) /\ v e. CC) /\ (y +h z) = (v .h y)) -> (v + -u1) e. CC)
44		hvsubadd 9027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((v .h y) e. H~ /\ y e. H~ /\ z e. H~) -> (((v .h y) -h y) = z <-> (y +h z) = (v .h y)))
45		hvmulcl 8966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e. CC /\ y e. H~) -> (v .h y) e. H~)
46	45	ancoms 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. H~ /\ v e. CC) -> (v .h y) e. H~)
47	46	adantlr 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> (v .h y) e. H~)
48		simpll 421	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> y e. H~)
49		simplr 422	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> z e. H~)
50	44, 47, 48, 49	syl3anc 870	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> (((v .h y) -h y) = z <-> (y +h z) = (v .h y)))
51	50	biimpar 426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((y e. H~ /\ z e. H~) /\ v e. CC) /\ (y +h z) = (v .h y)) -> ((v .h y) -h y) = z)
52		hvsubval 8969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((v .h y) e. H~ /\ y e. H~) -> ((v .h y) -h y) = ((v .h y) +h (-u1 .h y)))
53	45, 52	sylancom 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e.