Metamath Proof Explorer

Theorem cdjreui

Description: A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of Holland p. 1520. (Contributed by NM, 20-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdjreu.1 
|- A e. SH
cdjreu.2 
|- B e. SH
Assertion cdjreui 
|- ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> E! x e. A E. y e. B C = ( x +h y ) )

Proof

Step Hyp Ref Expression
1 cdjreu.1 
 |-  A e. SH
2 cdjreu.2 
 |-  B e. SH
3 1 2 shseli 
 |-  ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) )
4 3 biimpi 
 |-  ( C e. ( A +H B ) -> E. x e. A E. y e. B C = ( x +h y ) )
5 reeanv 
 |-  ( E. y e. B E. w e. B ( C = ( x +h y ) /\ C = ( z +h w ) ) <-> ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) )
6 eqtr2 
 |-  ( ( C = ( x +h y ) /\ C = ( z +h w ) ) -> ( x +h y ) = ( z +h w ) )
7 1 sheli 
 |-  ( x e. A -> x e. ~H )
8 2 sheli 
 |-  ( y e. B -> y e. ~H )
9 7 8 anim12i 
 |-  ( ( x e. A /\ y e. B ) -> ( x e. ~H /\ y e. ~H ) )
10 1 sheli 
 |-  ( z e. A -> z e. ~H )
11 2 sheli 
 |-  ( w e. B -> w e. ~H )
12 10 11 anim12i 
 |-  ( ( z e. A /\ w e. B ) -> ( z e. ~H /\ w e. ~H ) )
13 hvaddsub4 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( x +h y ) = ( z +h w ) <-> ( x -h z ) = ( w -h y ) ) )
14 9 12 13 syl2an 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( z e. A /\ w e. B ) ) -> ( ( x +h y ) = ( z +h w ) <-> ( x -h z ) = ( w -h y ) ) )
15 14 an4s 
 |-  ( ( ( x e. A /\ z e. A ) /\ ( y e. B /\ w e. B ) ) -> ( ( x +h y ) = ( z +h w ) <-> ( x -h z ) = ( w -h y ) ) )
16 15 adantll 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( x +h y ) = ( z +h w ) <-> ( x -h z ) = ( w -h y ) ) )
17 shsubcl 
 |-  ( ( B e. SH /\ w e. B /\ y e. B ) -> ( w -h y ) e. B )
18 2 17 mp3an1 
 |-  ( ( w e. B /\ y e. B ) -> ( w -h y ) e. B )
19 18 ancoms 
 |-  ( ( y e. B /\ w e. B ) -> ( w -h y ) e. B )
20 eleq1 
 |-  ( ( x -h z ) = ( w -h y ) -> ( ( x -h z ) e. B <-> ( w -h y ) e. B ) )
21 19 20 syl5ibrcom 
 |-  ( ( y e. B /\ w e. B ) -> ( ( x -h z ) = ( w -h y ) -> ( x -h z ) e. B ) )
22 21 adantl 
 |-  ( ( ( x e. A /\ z e. A ) /\ ( y e. B /\ w e. B ) ) -> ( ( x -h z ) = ( w -h y ) -> ( x -h z ) e. B ) )
23 shsubcl 
 |-  ( ( A e. SH /\ x e. A /\ z e. A ) -> ( x -h z ) e. A )
24 1 23 mp3an1 
 |-  ( ( x e. A /\ z e. A ) -> ( x -h z ) e. A )
25 24 adantr 
 |-  ( ( ( x e. A /\ z e. A ) /\ ( y e. B /\ w e. B ) ) -> ( x -h z ) e. A )
26 22 25 jctild 
 |-  ( ( ( x e. A /\ z e. A ) /\ ( y e. B /\ w e. B ) ) -> ( ( x -h z ) = ( w -h y ) -> ( ( x -h z ) e. A /\ ( x -h z ) e. B ) ) )
27 26 adantll 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( x -h z ) = ( w -h y ) -> ( ( x -h z ) e. A /\ ( x -h z ) e. B ) ) )
28 elin 
 |-  ( ( x -h z ) e. ( A i^i B ) <-> ( ( x -h z ) e. A /\ ( x -h z ) e. B ) )
29 eleq2 
 |-  ( ( A i^i B ) = 0H -> ( ( x -h z ) e. ( A i^i B ) <-> ( x -h z ) e. 0H ) )
30 28 29 bitr3id 
 |-  ( ( A i^i B ) = 0H -> ( ( ( x -h z ) e. A /\ ( x -h z ) e. B ) <-> ( x -h z ) e. 0H ) )
31 30 ad2antrr 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( ( x -h z ) e. A /\ ( x -h z ) e. B ) <-> ( x -h z ) e. 0H ) )
32 27 31 sylibd 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( x -h z ) = ( w -h y ) -> ( x -h z ) e. 0H ) )
33 elch0 
 |-  ( ( x -h z ) e. 0H <-> ( x -h z ) = 0h )
34 hvsubeq0 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( x -h z ) = 0h <-> x = z ) )
35 33 34 bitrid 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( x -h z ) e. 0H <-> x = z ) )
36 7 10 35 syl2an 
 |-  ( ( x e. A /\ z e. A ) -> ( ( x -h z ) e. 0H <-> x = z ) )
37 36 ad2antlr 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( x -h z ) e. 0H <-> x = z ) )
38 32 37 sylibd 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( x -h z ) = ( w -h y ) -> x = z ) )
39 16 38 sylbid 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( x +h y ) = ( z +h w ) -> x = z ) )
40 6 39 syl5 
 |-  ( ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) /\ ( y e. B /\ w e. B ) ) -> ( ( C = ( x +h y ) /\ C = ( z +h w ) ) -> x = z ) )
41 40 rexlimdvva 
 |-  ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) -> ( E. y e. B E. w e. B ( C = ( x +h y ) /\ C = ( z +h w ) ) -> x = z ) )
42 5 41 biimtrrid 
 |-  ( ( ( A i^i B ) = 0H /\ ( x e. A /\ z e. A ) ) -> ( ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) -> x = z ) )
43 42 ralrimivva 
 |-  ( ( A i^i B ) = 0H -> A. x e. A A. z e. A ( ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) -> x = z ) )
44 4 43 anim12i 
 |-  ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> ( E. x e. A E. y e. B C = ( x +h y ) /\ A. x e. A A. z e. A ( ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) -> x = z ) ) )
45 oveq1 
 |-  ( x = z -> ( x +h y ) = ( z +h y ) )
46 45 eqeq2d 
 |-  ( x = z -> ( C = ( x +h y ) <-> C = ( z +h y ) ) )
47 46 rexbidv 
 |-  ( x = z -> ( E. y e. B C = ( x +h y ) <-> E. y e. B C = ( z +h y ) ) )
48 oveq2 
 |-  ( y = w -> ( z +h y ) = ( z +h w ) )
49 48 eqeq2d 
 |-  ( y = w -> ( C = ( z +h y ) <-> C = ( z +h w ) ) )
50 49 cbvrexvw 
 |-  ( E. y e. B C = ( z +h y ) <-> E. w e. B C = ( z +h w ) )
51 47 50 bitrdi 
 |-  ( x = z -> ( E. y e. B C = ( x +h y ) <-> E. w e. B C = ( z +h w ) ) )
52 51 reu4 
 |-  ( E! x e. A E. y e. B C = ( x +h y ) <-> ( E. x e. A E. y e. B C = ( x +h y ) /\ A. x e. A A. z e. A ( ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) -> x = z ) ) )
53 44 52 sylibr 
 |-  ( ( C e. ( A +H B ) /\ ( A i^i B ) = 0H ) -> E! x e. A E. y e. B C = ( x +h y ) )