Metamath Proof Explorer

Theorem sumdmdii

Description: If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in MaedaMaeda p. 139. (Contributed by NM, 12-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 
|- A e. CH
sumdmdi.2 
|- B e. CH
Assertion sumdmdii 
|- ( ( A +H B ) = ( A vH B ) -> A MH* B )

Proof

Step Hyp Ref Expression
1 sumdmdi.1 
 |-  A e. CH
2 sumdmdi.2 
 |-  B e. CH
3 ineq2 
 |-  ( ( A +H B ) = ( A vH B ) -> ( x i^i ( A +H B ) ) = ( x i^i ( A vH B ) ) )
4 3 adantr 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ ( x e. CH /\ B C_ x ) ) -> ( x i^i ( A +H B ) ) = ( x i^i ( A vH B ) ) )
5 elin 
 |-  ( y e. ( x i^i ( A +H B ) ) <-> ( y e. x /\ y e. ( A +H B ) ) )
6 1 2 chseli 
 |-  ( y e. ( A +H B ) <-> E. z e. A E. w e. B y = ( z +h w ) )
7 ssel2 
 |-  ( ( B C_ x /\ w e. B ) -> w e. x )
8 chsh 
 |-  ( x e. CH -> x e. SH )
9 shsubcl 
 |-  ( ( x e. SH /\ y e. x /\ w e. x ) -> ( y -h w ) e. x )
10 9 3exp 
 |-  ( x e. SH -> ( y e. x -> ( w e. x -> ( y -h w ) e. x ) ) )
11 8 10 syl 
 |-  ( x e. CH -> ( y e. x -> ( w e. x -> ( y -h w ) e. x ) ) )
12 7 11 syl7 
 |-  ( x e. CH -> ( y e. x -> ( ( B C_ x /\ w e. B ) -> ( y -h w ) e. x ) ) )
13 12 exp4a 
 |-  ( x e. CH -> ( y e. x -> ( B C_ x -> ( w e. B -> ( y -h w ) e. x ) ) ) )
14 13 com23 
 |-  ( x e. CH -> ( B C_ x -> ( y e. x -> ( w e. B -> ( y -h w ) e. x ) ) ) )
15 14 imp41 
 |-  ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ w e. B ) -> ( y -h w ) e. x )
16 15 adantlr 
 |-  ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) -> ( y -h w ) e. x )
17 16 adantr 
 |-  ( ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) /\ y = ( z +h w ) ) -> ( y -h w ) e. x )
18 chel 
 |-  ( ( x e. CH /\ y e. x ) -> y e. ~H )
19 18 adantlr 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> y e. ~H )
20 1 cheli 
 |-  ( z e. A -> z e. ~H )
21 2 cheli 
 |-  ( w e. B -> w e. ~H )
22 hvsubadd 
 |-  ( ( y e. ~H /\ w e. ~H /\ z e. ~H ) -> ( ( y -h w ) = z <-> ( w +h z ) = y ) )
23 ax-hvcom 
 |-  ( ( w e. ~H /\ z e. ~H ) -> ( w +h z ) = ( z +h w ) )
24 23 eqeq1d 
 |-  ( ( w e. ~H /\ z e. ~H ) -> ( ( w +h z ) = y <-> ( z +h w ) = y ) )
25 eqcom 
 |-  ( ( z +h w ) = y <-> y = ( z +h w ) )
26 24 25 syl6bb 
 |-  ( ( w e. ~H /\ z e. ~H ) -> ( ( w +h z ) = y <-> y = ( z +h w ) ) )
27 26 3adant1 
 |-  ( ( y e. ~H /\ w e. ~H /\ z e. ~H ) -> ( ( w +h z ) = y <-> y = ( z +h w ) ) )
28 22 27 bitrd 
 |-  ( ( y e. ~H /\ w e. ~H /\ z e. ~H ) -> ( ( y -h w ) = z <-> y = ( z +h w ) ) )
29 28 3com23 
 |-  ( ( y e. ~H /\ z e. ~H /\ w e. ~H ) -> ( ( y -h w ) = z <-> y = ( z +h w ) ) )
30 19 20 21 29 syl3an 
 |-  ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A /\ w e. B ) -> ( ( y -h w ) = z <-> y = ( z +h w ) ) )
31 30 3expa 
 |-  ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) -> ( ( y -h w ) = z <-> y = ( z +h w ) ) )
32 eleq1 
 |-  ( ( y -h w ) = z -> ( ( y -h w ) e. x <-> z e. x ) )
33 31 32 syl6bir 
 |-  ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) -> ( y = ( z +h w ) -> ( ( y -h w ) e. x <-> z e. x ) ) )
34 33 imp 
 |-  ( ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) /\ y = ( z +h w ) ) -> ( ( y -h w ) e. x <-> z e. x ) )
35 17 34 mpbid 
 |-  ( ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) /\ y = ( z +h w ) ) -> z e. x )
36 simpr 
 |-  ( ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) /\ y = ( z +h w ) ) -> y = ( z +h w ) )
37 35 36 jca 
 |-  ( ( ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) /\ w e. B ) /\ y = ( z +h w ) ) -> ( z e. x /\ y = ( z +h w ) ) )
38 37 exp31 
 |-  ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) -> ( w e. B -> ( y = ( z +h w ) -> ( z e. x /\ y = ( z +h w ) ) ) ) )
39 38 reximdvai 
 |-  ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) -> ( E. w e. B y = ( z +h w ) -> E. w e. B ( z e. x /\ y = ( z +h w ) ) ) )
40 r19.42v 
 |-  ( E. w e. B ( z e. x /\ y = ( z +h w ) ) <-> ( z e. x /\ E. w e. B y = ( z +h w ) ) )
41 39 40 syl6ib 
 |-  ( ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) /\ z e. A ) -> ( E. w e. B y = ( z +h w ) -> ( z e. x /\ E. w e. B y = ( z +h w ) ) ) )
42 41 reximdva 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> ( E. z e. A E. w e. B y = ( z +h w ) -> E. z e. A ( z e. x /\ E. w e. B y = ( z +h w ) ) ) )
43 elin 
 |-  ( z e. ( x i^i A ) <-> ( z e. x /\ z e. A ) )
44 ancom 
 |-  ( ( z e. x /\ z e. A ) <-> ( z e. A /\ z e. x ) )
45 43 44 bitri 
 |-  ( z e. ( x i^i A ) <-> ( z e. A /\ z e. x ) )
46 45 anbi1i 
 |-  ( ( z e. ( x i^i A ) /\ E. w e. B y = ( z +h w ) ) <-> ( ( z e. A /\ z e. x ) /\ E. w e. B y = ( z +h w ) ) )
47 anass 
 |-  ( ( ( z e. A /\ z e. x ) /\ E. w e. B y = ( z +h w ) ) <-> ( z e. A /\ ( z e. x /\ E. w e. B y = ( z +h w ) ) ) )
48 46 47 bitri 
 |-  ( ( z e. ( x i^i A ) /\ E. w e. B y = ( z +h w ) ) <-> ( z e. A /\ ( z e. x /\ E. w e. B y = ( z +h w ) ) ) )
49 48 rexbii2 
 |-  ( E. z e. ( x i^i A ) E. w e. B y = ( z +h w ) <-> E. z e. A ( z e. x /\ E. w e. B y = ( z +h w ) ) )
50 42 49 syl6ibr 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> ( E. z e. A E. w e. B y = ( z +h w ) -> E. z e. ( x i^i A ) E. w e. B y = ( z +h w ) ) )
51 1 chshii 
 |-  A e. SH
52 shincl 
 |-  ( ( x e. SH /\ A e. SH ) -> ( x i^i A ) e. SH )
53 8 51 52 sylancl 
 |-  ( x e. CH -> ( x i^i A ) e. SH )
54 53 ad2antrr 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> ( x i^i A ) e. SH )
55 2 chshii 
 |-  B e. SH
56 shsel 
 |-  ( ( ( x i^i A ) e. SH /\ B e. SH ) -> ( y e. ( ( x i^i A ) +H B ) <-> E. z e. ( x i^i A ) E. w e. B y = ( z +h w ) ) )
57 54 55 56 sylancl 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> ( y e. ( ( x i^i A ) +H B ) <-> E. z e. ( x i^i A ) E. w e. B y = ( z +h w ) ) )
58 50 57 sylibrd 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> ( E. z e. A E. w e. B y = ( z +h w ) -> y e. ( ( x i^i A ) +H B ) ) )
59 6 58 syl5bi 
 |-  ( ( ( x e. CH /\ B C_ x ) /\ y e. x ) -> ( y e. ( A +H B ) -> y e. ( ( x i^i A ) +H B ) ) )
60 59 expimpd 
 |-  ( ( x e. CH /\ B C_ x ) -> ( ( y e. x /\ y e. ( A +H B ) ) -> y e. ( ( x i^i A ) +H B ) ) )
61 5 60 syl5bi 
 |-  ( ( x e. CH /\ B C_ x ) -> ( y e. ( x i^i ( A +H B ) ) -> y e. ( ( x i^i A ) +H B ) ) )
62 61 ssrdv 
 |-  ( ( x e. CH /\ B C_ x ) -> ( x i^i ( A +H B ) ) C_ ( ( x i^i A ) +H B ) )
63 62 adantl 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ ( x e. CH /\ B C_ x ) ) -> ( x i^i ( A +H B ) ) C_ ( ( x i^i A ) +H B ) )
64 4 63 eqsstrrd 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ ( x e. CH /\ B C_ x ) ) -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) +H B ) )
65 chincl 
 |-  ( ( x e. CH /\ A e. CH ) -> ( x i^i A ) e. CH )
66 1 65 mpan2 
 |-  ( x e. CH -> ( x i^i A ) e. CH )
67 chslej 
 |-  ( ( ( x i^i A ) e. CH /\ B e. CH ) -> ( ( x i^i A ) +H B ) C_ ( ( x i^i A ) vH B ) )
68 66 2 67 sylancl 
 |-  ( x e. CH -> ( ( x i^i A ) +H B ) C_ ( ( x i^i A ) vH B ) )
69 68 ad2antrl 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ ( x e. CH /\ B C_ x ) ) -> ( ( x i^i A ) +H B ) C_ ( ( x i^i A ) vH B ) )
70 64 69 sstrd 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ ( x e. CH /\ B C_ x ) ) -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) )
71 70 exp32 
 |-  ( ( A +H B ) = ( A vH B ) -> ( x e. CH -> ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) ) )
72 71 ralrimiv 
 |-  ( ( A +H B ) = ( A vH B ) -> A. x e. CH ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) )
73 dmdbr2 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) ) )
74 1 2 73 mp2an 
 |-  ( A MH* B <-> A. x e. CH ( B C_ x -> ( x i^i ( A vH B ) ) C_ ( ( x i^i A ) vH B ) ) )
75 72 74 sylibr 
 |-  ( ( A +H B ) = ( A vH B ) -> A MH* B )