Metamath Proof Explorer

Theorem sumdmdlem2

Description: Lemma for sumdmdi . (Contributed by NM, 23-Dec-2004) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 
|- A e. CH
sumdmdi.2 
|- B e. CH
Assertion sumdmdlem2 
|- ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( A +H B ) = ( A vH B ) )

Proof

Step Hyp Ref Expression
1 sumdmdi.1 
 |-  A e. CH
2 sumdmdi.2 
 |-  B e. CH
3 1 2 chjcli 
 |-  ( A vH B ) e. CH
4 3 cheli 
 |-  ( y e. ( A vH B ) -> y e. ~H )
5 spansnsh 
 |-  ( y e. ~H -> ( span ` { y } ) e. SH )
6 2 chshii 
 |-  B e. SH
7 shsub2 
 |-  ( ( ( span ` { y } ) e. SH /\ B e. SH ) -> ( span ` { y } ) C_ ( B +H ( span ` { y } ) ) )
8 5 6 7 sylancl 
 |-  ( y e. ~H -> ( span ` { y } ) C_ ( B +H ( span ` { y } ) ) )
9 spansnid 
 |-  ( y e. ~H -> y e. ( span ` { y } ) )
10 8 9 sseldd 
 |-  ( y e. ~H -> y e. ( B +H ( span ` { y } ) ) )
11 10 ad2antrl 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> y e. ( B +H ( span ` { y } ) ) )
12 elin 
 |-  ( y e. ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) <-> ( y e. ( B +H ( span ` { y } ) ) /\ y e. ( A vH B ) ) )
13 df-ne 
 |-  ( y =/= 0h <-> -. y = 0h )
14 spansna 
 |-  ( ( y e. ~H /\ y =/= 0h ) -> ( span ` { y } ) e. HAtoms )
15 13 14 sylan2br 
 |-  ( ( y e. ~H /\ -. y = 0h ) -> ( span ` { y } ) e. HAtoms )
16 oveq1 
 |-  ( x = ( span ` { y } ) -> ( x vH B ) = ( ( span ` { y } ) vH B ) )
17 16 ineq1d 
 |-  ( x = ( span ` { y } ) -> ( ( x vH B ) i^i ( A vH B ) ) = ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) )
18 16 ineq1d 
 |-  ( x = ( span ` { y } ) -> ( ( x vH B ) i^i A ) = ( ( ( span ` { y } ) vH B ) i^i A ) )
19 18 oveq1d 
 |-  ( x = ( span ` { y } ) -> ( ( ( x vH B ) i^i A ) vH B ) = ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) )
20 17 19 sseq12d 
 |-  ( x = ( span ` { y } ) -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) <-> ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) C_ ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) ) )
21 20 rspcv 
 |-  ( ( span ` { y } ) e. HAtoms -> ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) C_ ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) ) )
22 15 21 syl 
 |-  ( ( y e. ~H /\ -. y = 0h ) -> ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) C_ ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) ) )
23 spansnj 
 |-  ( ( B e. CH /\ y e. ~H ) -> ( B +H ( span ` { y } ) ) = ( B vH ( span ` { y } ) ) )
24 spansnch 
 |-  ( y e. ~H -> ( span ` { y } ) e. CH )
25 chjcom 
 |-  ( ( B e. CH /\ ( span ` { y } ) e. CH ) -> ( B vH ( span ` { y } ) ) = ( ( span ` { y } ) vH B ) )
26 24 25 sylan2 
 |-  ( ( B e. CH /\ y e. ~H ) -> ( B vH ( span ` { y } ) ) = ( ( span ` { y } ) vH B ) )
27 23 26 eqtrd 
 |-  ( ( B e. CH /\ y e. ~H ) -> ( B +H ( span ` { y } ) ) = ( ( span ` { y } ) vH B ) )
28 2 27 mpan 
 |-  ( y e. ~H -> ( B +H ( span ` { y } ) ) = ( ( span ` { y } ) vH B ) )
29 28 ineq1d 
 |-  ( y e. ~H -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) = ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) )
30 28 ineq1d 
 |-  ( y e. ~H -> ( ( B +H ( span ` { y } ) ) i^i A ) = ( ( ( span ` { y } ) vH B ) i^i A ) )
31 30 oveq1d 
 |-  ( y e. ~H -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) = ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) )
32 29 31 sseq12d 
 |-  ( y e. ~H -> ( ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) <-> ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) C_ ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) ) )
33 32 adantr 
 |-  ( ( y e. ~H /\ -. y = 0h ) -> ( ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) <-> ( ( ( span ` { y } ) vH B ) i^i ( A vH B ) ) C_ ( ( ( ( span ` { y } ) vH B ) i^i A ) vH B ) ) )
34 22 33 sylibrd 
 |-  ( ( y e. ~H /\ -. y = 0h ) -> ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) ) )
35 34 com12 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( ( y e. ~H /\ -. y = 0h ) -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) ) )
36 35 expdimp 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ y e. ~H ) -> ( -. y = 0h -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) ) )
37 ssid 
 |-  B C_ B
38 sneq 
 |-  ( y = 0h -> { y } = { 0h } )
39 38 fveq2d 
 |-  ( y = 0h -> ( span ` { y } ) = ( span ` { 0h } ) )
40 spansn0 
 |-  ( span ` { 0h } ) = 0H
41 39 40 eqtrdi 
 |-  ( y = 0h -> ( span ` { y } ) = 0H )
42 41 oveq2d 
 |-  ( y = 0h -> ( B +H ( span ` { y } ) ) = ( B +H 0H ) )
43 6 shs0i 
 |-  ( B +H 0H ) = B
44 42 43 eqtrdi 
 |-  ( y = 0h -> ( B +H ( span ` { y } ) ) = B )
45 44 ineq1d 
 |-  ( y = 0h -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) = ( B i^i ( A vH B ) ) )
46 inss1 
 |-  ( B i^i ( A vH B ) ) C_ B
47 2 1 chub2i 
 |-  B C_ ( A vH B )
48 37 47 ssini 
 |-  B C_ ( B i^i ( A vH B ) )
49 46 48 eqssi 
 |-  ( B i^i ( A vH B ) ) = B
50 45 49 eqtrdi 
 |-  ( y = 0h -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) = B )
51 44 ineq1d 
 |-  ( y = 0h -> ( ( B +H ( span ` { y } ) ) i^i A ) = ( B i^i A ) )
52 51 oveq1d 
 |-  ( y = 0h -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) = ( ( B i^i A ) vH B ) )
53 2 1 chincli 
 |-  ( B i^i A ) e. CH
54 53 2 chjcomi 
 |-  ( ( B i^i A ) vH B ) = ( B vH ( B i^i A ) )
55 2 1 chabs1i 
 |-  ( B vH ( B i^i A ) ) = B
56 54 55 eqtri 
 |-  ( ( B i^i A ) vH B ) = B
57 52 56 eqtrdi 
 |-  ( y = 0h -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) = B )
58 50 57 sseq12d 
 |-  ( y = 0h -> ( ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) <-> B C_ B ) )
59 37 58 mpbiri 
 |-  ( y = 0h -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) )
60 36 59 pm2.61d2 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ y e. ~H ) -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) )
61 60 adantrr 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) )
62 1 2 sumdmdlem 
 |-  ( ( y e. ~H /\ -. y e. ( A +H B ) ) -> ( ( B +H ( span ` { y } ) ) i^i A ) = ( B i^i A ) )
63 62 oveq1d 
 |-  ( ( y e. ~H /\ -. y e. ( A +H B ) ) -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) = ( ( B i^i A ) vH B ) )
64 63 56 eqtrdi 
 |-  ( ( y e. ~H /\ -. y e. ( A +H B ) ) -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) = B )
65 1 chshii 
 |-  A e. SH
66 6 65 shsub2i 
 |-  B C_ ( A +H B )
67 64 66 eqsstrdi 
 |-  ( ( y e. ~H /\ -. y e. ( A +H B ) ) -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) C_ ( A +H B ) )
68 67 adantl 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> ( ( ( B +H ( span ` { y } ) ) i^i A ) vH B ) C_ ( A +H B ) )
69 61 68 sstrd 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) C_ ( A +H B ) )
70 69 sseld 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> ( y e. ( ( B +H ( span ` { y } ) ) i^i ( A vH B ) ) -> y e. ( A +H B ) ) )
71 12 70 biimtrrid 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> ( ( y e. ( B +H ( span ` { y } ) ) /\ y e. ( A vH B ) ) -> y e. ( A +H B ) ) )
72 11 71 mpand 
 |-  ( ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) /\ ( y e. ~H /\ -. y e. ( A +H B ) ) ) -> ( y e. ( A vH B ) -> y e. ( A +H B ) ) )
73 72 exp32 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( y e. ~H -> ( -. y e. ( A +H B ) -> ( y e. ( A vH B ) -> y e. ( A +H B ) ) ) ) )
74 73 com34 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( y e. ~H -> ( y e. ( A vH B ) -> ( -. y e. ( A +H B ) -> y e. ( A +H B ) ) ) ) )
75 pm2.18 
 |-  ( ( -. y e. ( A +H B ) -> y e. ( A +H B ) ) -> y e. ( A +H B ) )
76 74 75 syl8 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( y e. ~H -> ( y e. ( A vH B ) -> y e. ( A +H B ) ) ) )
77 4 76 syl5 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( y e. ( A vH B ) -> ( y e. ( A vH B ) -> y e. ( A +H B ) ) ) )
78 77 pm2.43d 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( y e. ( A vH B ) -> y e. ( A +H B ) ) )
79 78 ssrdv 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( A vH B ) C_ ( A +H B ) )
80 1 2 chsleji 
 |-  ( A +H B ) C_ ( A vH B )
81 79 80 jctil 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( ( A +H B ) C_ ( A vH B ) /\ ( A vH B ) C_ ( A +H B ) ) )
82 eqss 
 |-  ( ( A +H B ) = ( A vH B ) <-> ( ( A +H B ) C_ ( A vH B ) /\ ( A vH B ) C_ ( A +H B ) ) )
83 81 82 sylibr 
 |-  ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( A +H B ) = ( A vH B ) )