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 bitrdi
 |-  ( ( 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 )