Theorem chocuni 5179

Description: Lemma for uniqueness part of Projection Theorem. Theorem 3.7(i) of [Beran] p. 102 (uniqueness part).

Hypothesis

Ref	Expression
chocuni.1	|- H e. CH

Assertion

Ref	Expression
chocuni	|- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((R = (A +v B) /\ R = (C +v D)) -> (A = C /\ B = D)))

Proof of Theorem chocuni

Step	Hyp	Ref	Expression
1		hvsub4t 5014	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ (A e. H~ /\ D e. H~)) -> ((A +v B) -v (A +v D)) = ((A -v A) +v (B -v D)))
2		pm3.26 256	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (A e. H~ /\ B e. H~))
3		pm3.26 256	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~) -> A e. H~)
4	3	anim1i 269	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (A e. H~ /\ D e. H~))
5	1, 2, 4	sylanc 361	. . . . . . 7 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> ((A +v B) -v (A +v D)) = ((A -v A) +v (B -v D)))
6		hvsubidt 5005	. . . . . . . . 9 |- (A e. H~ -> (A -v A) = 0v)
7	6	ad2antll 320	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (A -v A) = 0v)
8	7	opreq1d 3012	. . . . . . 7 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> ((A -v A) +v (B -v D)) = (0v +v (B -v D)))
9		hvsubclt 4998	. . . . . . . . 9 |- ((B e. H~ /\ D e. H~) -> (B -v D) e. H~)
10		hvaddid2t 5003	. . . . . . . . 9 |- ((B -v D) e. H~ -> (0v +v (B -v D)) = (B -v D))
11	9, 10	syl 12	. . . . . . . 8 |- ((B e. H~ /\ D e. H~) -> (0v +v (B -v D)) = (B -v D))
12	11	adantll 309	. . . . . . 7 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (0v +v (B -v D)) = (B -v D))
13	5, 8, 12	3eqtrd 1132	. . . . . 6 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> ((A +v B) -v (A +v D)) = (B -v D))
14	13	adantrl 311	. . . . 5 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A +v B) -v (A +v D)) = (B -v D))
15		hvsub4t 5014	. . . . . . . 8 |- (((C e. H~ /\ D e. H~) /\ (A e. H~ /\ D e. H~)) -> ((C +v D) -v (A +v D)) = ((C -v A) +v (D -v D)))
16		pm3.27 260	. . . . . . . 8 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> (C e. H~ /\ D e. H~))
17		pm3.27 260	. . . . . . . . 9 |- ((C e. H~ /\ D e. H~) -> D e. H~)
18	17	anim2i 270	. . . . . . . 8 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> (A e. H~ /\ D e. H~))
19	15, 16, 18	sylanc 361	. . . . . . 7 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C +v D) -v (A +v D)) = ((C -v A) +v (D -v D)))
20		hvsubidt 5005	. . . . . . . . 9 |- (D e. H~ -> (D -v D) = 0v)
21	20	ad2antrr 323	. . . . . . . 8 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> (D -v D) = 0v)
22	21	opreq2d 3013	. . . . . . 7 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C -v A) +v (D -v D)) = ((C -v A) +v 0v))
23		hvsubclt 4998	. . . . . . . . . 10 |- ((C e. H~ /\ A e. H~) -> (C -v A) e. H~)
24		ax-hvaddid 4988	. . . . . . . . . 10 |- ((C -v A) e. H~ -> ((C -v A) +v 0v) = (C -v A))
25	23, 24	syl 12	. . . . . . . . 9 |- ((C e. H~ /\ A e. H~) -> ((C -v A) +v 0v) = (C -v A))
26	25	ancoms 334	. . . . . . . 8 |- ((A e. H~ /\ C e. H~) -> ((C -v A) +v 0v) = (C -v A))
27	26	adantrr 312	. . . . . . 7 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C -v A) +v 0v) = (C -v A))
28	19, 22, 27	3eqtrd 1132	. . . . . 6 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C +v D) -v (A +v D)) = (C -v A))
29	28	adantlr 310	. . . . 5 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((C +v D) -v (A +v D)) = (C -v A))
30	14, 29	cleq12d 1115	. . . 4 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (((A +v B) -v (A +v D)) = ((C +v D) -v (A +v D)) <-> (B -v D) = (C -v A)))
31		chocuni.1	. . . . . 6 |- H e. CH
32	31	chel 5137	. . . . 5 |- (A e. H -> A e. H~)
33	31	chshi 5132	. . . . . . 7 |- H e. SH
34		shocsh 5165	. . . . . . 7 |- (H e. SH -> (_|_` H) e. SH)
35	33, 34	ax-mp 6	. . . . . 6 |- (_|_` H) e. SH
36	35	shel 5120	. . . . 5 |- (B e. (_|_` H) -> B e. H~)
37	32, 36	anim12i 268	. . . 4 |- ((A e. H /\ B e. (_|_` H)) -> (A e. H~ /\ B e. H~))
38	31	chel 5137	. . . . 5 |- (C e. H -> C e. H~)
39	35	shel 5120	. . . . 5 |- (D e. (_|_` H) -> D e. H~)
40	38, 39	anim12i 268	. . . 4 |- ((C e. H /\ D e. (_|_` H)) -> (C e. H~ /\ D e. H~))
41	30, 37, 40	syl2an 349	. . 3 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> (((A +v B) -v (A +v D)) = ((C +v D) -v (A +v D)) <-> (B -v D) = (C -v A)))
42		shsubclt 5125	. . . . . . . . . . 11 |- (H e. SH -> ((C e. H /\ A e. H) -> (C -v A) e. H))
43	33, 42	ax-mp 6	. . . . . . . . . 10 |- ((C e. H /\ A e. H) -> (C -v A) e. H)
44	43	ancoms 334	. . . . . . . . 9 |- ((A e. H /\ C e. H) -> (C -v A) e. H)
45	44	a1d 14	. . . . . . . 8 |- ((A e. H /\ C e. H) -> ((B -v D) = (C -v A) -> (C -v A) e. H))
46	45	adantrr 312	. . . . . . 7 |- ((A e. H /\ (C e. H /\ D e. (_|_` H))) -> ((B -v D) = (C -v A) -> (C -v A) e. H))
47	46	adantlr 310	. . . . . 6 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((B -v D) = (C -v A) -> (C -v A) e. H))
48		shsubclt 5125	. . . . . . . . . 10 |- ((_|_` H) e. SH -> ((B e. (_|_` H) /\ D e. (_|_` H)) -> (B -v D) e. (_|_` H)))
49	35, 48	ax-mp 6	. . . . . . . . 9 |- ((B e. (_|_` H) /\ D e. (_|_` H)) -> (B -v D) e. (_|_` H))
50		eleq1 1149	. . . . . . . . . 10 |- ((B -v D) = (C -v A) -> ((B -v D) e. (_|_` H) <-> (C -v A) e. (_|_` H)))
51	50	biimpcd 137	. . . . . . . . 9 |- ((B -v D) e. (_|_` H) -> ((B -v D) = (C -v A) -> (C -v A) e. (_|_` H)))
52	49, 51	syl 12	. . . . . . . 8 |- ((B e. (_|_` H) /\ D e. (_|_` H)) -> ((B -v D) = (C -v A) -> (C -v A) e. (_|_` H)))
53	52	adantrl 311	. . . . . . 7 |- ((B e. (_|_` H) /\ (C e. H /\ D e. (_|_` H))) -> ((B -v D) = (C -v A) -> (C -v A) e. (_|_` H)))
54	53	adantll 309	. . . . . 6 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((B -v D) = (C -v A) -> (C -v A) e. (_|_` H)))
55	47, 54	jcad 455	. . . . 5 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((B -v D) = (C -v A) -> ((C -v A) e. H /\ (C -v A) e. (_|_` H))))
56		hvsubeq0t 5040	. . . . . . . . . . 11 |- ((C e. H~ /\ A e. H~) -> ((C -v A) = 0v <-> C = A))
57	56	ancoms 334	. . . . . . . . . 10 |- ((A e. H~ /\ C e. H~) -> ((C -v A) = 0v <-> C = A))
58	57	adantrr 312	. . . . . . . . 9 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C -v A) = 0v <-> C = A))
59	58	adantlr 310	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((C -v A) = 0v <-> C = A))
60	59, 37, 40	syl2an 349	. . . . . . 7 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((C -v A) = 0v <-> C = A))
61		cleqcom 1103	. . . . . . 7 |- (C = A <-> A = C)
62	60, 61	syl6bb 414	. . . . . 6 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((C -v A) = 0v <-> A = C))
63		ocin 5177	. . . . . . . . 9 |- (H e. SH -> (H i^i (_|_` H