Theorem chocuni 9127

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 +h B) /\ R = (C +h D)) -> (A = C /\ B = D)))

Proof of Theorem chocuni

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . . . . . . 9 |- ((A e. H~ /\ B e. H~) -> A e. H~)
2	1	anim1i 334	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (A e. H~ /\ D e. H~))
3		hvsub4t 8861	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ (A e. H~ /\ D e. H~)) -> ((A +h B) -h (A +h D)) = ((A -h A) +h (B -h D)))
4	2, 3	syldan 467	. . . . . . 7 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> ((A +h B) -h (A +h D)) = ((A -h A) +h (B -h D)))
5		hvsubidt 8850	. . . . . . . . 9 |- (A e. H~ -> (A -h A) = 0h)
6	5	ad2antrr 404	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (A -h A) = 0h)
7	6	opreq1d 3970	. . . . . . 7 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> ((A -h A) +h (B -h D)) = (0h +h (B -h D)))
8		hvsubclt 8842	. . . . . . . . 9 |- ((B e. H~ /\ D e. H~) -> (B -h D) e. H~)
9		hvaddid2t 8847	. . . . . . . . 9 |- ((B -h D) e. H~ -> (0h +h (B -h D)) = (B -h D))
10	8, 9	syl 10	. . . . . . . 8 |- ((B e. H~ /\ D e. H~) -> (0h +h (B -h D)) = (B -h D))
11	10	adantll 392	. . . . . . 7 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> (0h +h (B -h D)) = (B -h D))
12	4, 7, 11	3eqtrd 1509	. . . . . 6 |- (((A e. H~ /\ B e. H~) /\ D e. H~) -> ((A +h B) -h (A +h D)) = (B -h D))
13	12	adantrl 394	. . . . 5 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((A +h B) -h (A +h D)) = (B -h D))
14		hvsub4t 8861	. . . . . . . 8 |- (((C e. H~ /\ D e. H~) /\ (A e. H~ /\ D e. H~)) -> ((C +h D) -h (A +h D)) = ((C -h A) +h (D -h D)))
15		pm3.27 323	. . . . . . . 8 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> (C e. H~ /\ D e. H~))
16		pm3.27 323	. . . . . . . . 9 |- ((C e. H~ /\ D e. H~) -> D e. H~)
17	16	anim2i 335	. . . . . . . 8 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> (A e. H~ /\ D e. H~))
18	14, 15, 17	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C +h D) -h (A +h D)) = ((C -h A) +h (D -h D)))
19		hvsubidt 8850	. . . . . . . . 9 |- (D e. H~ -> (D -h D) = 0h)
20	19	ad2antll 407	. . . . . . . 8 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> (D -h D) = 0h)
21	20	opreq2d 3971	. . . . . . 7 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C -h A) +h (D -h D)) = ((C -h A) +h 0h))
22		hvsubclt 8842	. . . . . . . . . 10 |- ((C e. H~ /\ A e. H~) -> (C -h A) e. H~)
23		ax-hvaddid 8829	. . . . . . . . . 10 |- ((C -h A) e. H~ -> ((C -h A) +h 0h) = (C -h A))
24	22, 23	syl 10	. . . . . . . . 9 |- ((C e. H~ /\ A e. H~) -> ((C -h A) +h 0h) = (C -h A))
25	24	ancoms 436	. . . . . . . 8 |- ((A e. H~ /\ C e. H~) -> ((C -h A) +h 0h) = (C -h A))
26	25	adantrr 395	. . . . . . 7 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C -h A) +h 0h) = (C -h A))
27	18, 21, 26	3eqtrd 1509	. . . . . 6 |- ((A e. H~ /\ (C e. H~ /\ D e. H~)) -> ((C +h D) -h (A +h D)) = (C -h A))
28	27	adantlr 393	. . . . 5 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((C +h D) -h (A +h D)) = (C -h A))
29	13, 28	eqeq12d 1487	. . . 4 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> (((A +h B) -h (A +h D)) = ((C +h D) -h (A +h D)) <-> (B -h D) = (C -h A)))
30		chocuni.1	. . . . . 6 |- H e. CH
31	30	chel 9057	. . . . 5 |- (A e. H -> A e. H~)
32	30	chshi 9052	. . . . . . 7 |- H e. SH
33		shocsh 9112	. . . . . . 7 |- (H e. SH -> (_|_` H) e. SH)
34	32, 33	ax-mp 7	. . . . . 6 |- (_|_` H) e. SH
35	34	shel 9037	. . . . 5 |- (B e. (_|_` H) -> B e. H~)
36	31, 35	anim12i 333	. . . 4 |- ((A e. H /\ B e. (_|_` H)) -> (A e. H~ /\ B e. H~))
37	30	chel 9057	. . . . 5 |- (C e. H -> C e. H~)
38	34	shel 9037	. . . . 5 |- (D e. (_|_` H) -> D e. H~)
39	37, 38	anim12i 333	. . . 4 |- ((C e. H /\ D e. (_|_` H)) -> (C e. H~ /\ D e. H~))
40	29, 36, 39	syl2an 454	. . 3 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> (((A +h B) -h (A +h D)) = ((C +h D) -h (A +h D)) <-> (B -h D) = (C -h A)))
41		shsubcltOLD 9045	. . . . . . . . . 10 |- (H e. SH -> ((C e. H /\ A e. H) -> (C -h A) e. H))
42	32, 41	ax-mp 7	. . . . . . . . 9 |- ((C e. H /\ A e. H) -> (C -h A) e. H)
43	42	ancoms 436	. . . . . . . 8 |- ((A e. H /\ C e. H) -> (C -h A) e. H)
44	43	a1d 12	. . . . . . 7 |- ((A e. H /\ C e. H) -> ((B -h D) = (C -h A) -> (C -h A) e. H))
45	44	ad2ant2r 409	. . . . . 6 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((B -h D) = (C -h A) -> (C -h A) e. H))
46		eleq1 1532	. . . . . . . 8 |- ((B -h D) = (C -h A) -> ((B -h D) e. (_|_` H) <-> (C -h A) e. (_|_` H)))
47		shsubcltOLD 9045	. . . . . . . . 9 |- ((_|_` H) e. SH -> ((B e. (_|_` H) /\ D e. (_|_` H)) -> (B -h D) e. (_|_` H)))
48	34, 47	ax-mp 7	. . . . . . . 8 |- ((B e. (_|_` H) /\ D e. (_|_` H)) -> (B -h D) e. (_|_` H))
49	46, 48	syl5cbi 209	. . . . . . 7 |- ((B e. (_|_` H) /\ D e. (_|_` H)) -> ((B -h D) = (C -h A) -> (C -h A) e. (_|_` H)))
50	49	ad2ant2l 408	. . . . . 6 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((B -h D) = (C -h A) -> (C -h A) e. (_|_` H)))
51	45, 50	jcad 599	. . . . 5 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((B -h D) = (C -h A) -> ((C -h A) e. H /\ (C -h A) e. (_|_` H))))
52		hvsubeq0t 8890	. . . . . . . . . 10 |- ((C e. H~ /\ A e. H~) -> ((C -h A) = 0h <-> C = A))
53	52	ancoms 436	. . . . . . . . 9 |- ((A e. H~ /\ C e. H~) -> ((C -h A) = 0h <-> C = A))
54	53	ad2ant2r 409	. . . . . . . 8 |- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. H~)) -> ((C -h A) = 0h <-> C = A))
55	54, 36, 39	syl2an 454	. . . . . . 7 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((C -h A) = 0h <-> C = A))
56		eqcom 1475	. . . . . . 7 |- (C = A <-> A = C)
57	55, 56	syl6bb 535	. . . . . 6 |- (((A e. H /\ B e. (_|_` H)) /\ (C e. H /\ D e. (_|_` H))) -> ((C -h A) = 0h <-> A = C))
58		ocin 9124	. . . . . . . . 9 |- (H e. SH -> (H i^i (_|_` H)) = 0H)
59	32, 58	ax-mp 7	. . . . . . . 8 |- (H i^i (_|_` H)) = 0H
60	59	eleq2i 1536	. . . . . . 7 |- ((C -h A) e. (H i^i (_|_` H)) <-> (C -h A) e. 0H)
61		elin 2204	. . . . . . 7 |- ((C -h A) e. (H i^i (_|_` H)) <-> ((C -h A) e. H /\ (C -h A) e. (_|_` H)))
62		elch0 9081	. . . . . . 7 |- ((C -h A) e. 0H <-> (C -h A) = 0h)
63	60, 61, 62	3bitr3 181	. . . . . 6 |- (((C -h A) e. H /\ (C -h A) e. (_|_` H)