Metamath Proof Explorer

Theorem shmodsi

Description: The modular law holds for subspace sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 23-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shmod.1 
|- A e. SH
shmod.2 
|- B e. SH
shmod.3 
|- C e. SH
Assertion shmodsi 
|- ( A C_ C -> ( ( A +H B ) i^i C ) C_ ( A +H ( B i^i C ) ) )

Proof

Step Hyp Ref Expression
1 shmod.1 
 |-  A e. SH
2 shmod.2 
 |-  B e. SH
3 shmod.3 
 |-  C e. SH
4 elin 
 |-  ( z e. ( ( A +H B ) i^i C ) <-> ( z e. ( A +H B ) /\ z e. C ) )
5 1 2 shseli 
 |-  ( z e. ( A +H B ) <-> E. x e. A E. y e. B z = ( x +h y ) )
6 3 sheli 
 |-  ( z e. C -> z e. ~H )
7 1 sheli 
 |-  ( x e. A -> x e. ~H )
8 2 sheli 
 |-  ( y e. B -> y e. ~H )
9 hvsubadd 
 |-  ( ( z e. ~H /\ x e. ~H /\ y e. ~H ) -> ( ( z -h x ) = y <-> ( x +h y ) = z ) )
10 6 7 8 9 syl3an 
 |-  ( ( z e. C /\ x e. A /\ y e. B ) -> ( ( z -h x ) = y <-> ( x +h y ) = z ) )
11 eqcom 
 |-  ( ( x +h y ) = z <-> z = ( x +h y ) )
12 10 11 bitrdi 
 |-  ( ( z e. C /\ x e. A /\ y e. B ) -> ( ( z -h x ) = y <-> z = ( x +h y ) ) )
13 12 3expb 
 |-  ( ( z e. C /\ ( x e. A /\ y e. B ) ) -> ( ( z -h x ) = y <-> z = ( x +h y ) ) )
14 3 1 shsvsi 
 |-  ( ( z e. C /\ x e. A ) -> ( z -h x ) e. ( C +H A ) )
15 3 1 shscomi 
 |-  ( C +H A ) = ( A +H C )
16 14 15 eleqtrdi 
 |-  ( ( z e. C /\ x e. A ) -> ( z -h x ) e. ( A +H C ) )
17 1 3 shlesb1i 
 |-  ( A C_ C <-> ( A +H C ) = C )
18 17 biimpi 
 |-  ( A C_ C -> ( A +H C ) = C )
19 18 eleq2d 
 |-  ( A C_ C -> ( ( z -h x ) e. ( A +H C ) <-> ( z -h x ) e. C ) )
20 16 19 syl5ib 
 |-  ( A C_ C -> ( ( z e. C /\ x e. A ) -> ( z -h x ) e. C ) )
21 eleq1 
 |-  ( ( z -h x ) = y -> ( ( z -h x ) e. C <-> y e. C ) )
22 21 biimpd 
 |-  ( ( z -h x ) = y -> ( ( z -h x ) e. C -> y e. C ) )
23 20 22 sylan9 
 |-  ( ( A C_ C /\ ( z -h x ) = y ) -> ( ( z e. C /\ x e. A ) -> y e. C ) )
24 23 anim2d 
 |-  ( ( A C_ C /\ ( z -h x ) = y ) -> ( ( y e. B /\ ( z e. C /\ x e. A ) ) -> ( y e. B /\ y e. C ) ) )
25 elin 
 |-  ( y e. ( B i^i C ) <-> ( y e. B /\ y e. C ) )
26 24 25 syl6ibr 
 |-  ( ( A C_ C /\ ( z -h x ) = y ) -> ( ( y e. B /\ ( z e. C /\ x e. A ) ) -> y e. ( B i^i C ) ) )
27 26 ex 
 |-  ( A C_ C -> ( ( z -h x ) = y -> ( ( y e. B /\ ( z e. C /\ x e. A ) ) -> y e. ( B i^i C ) ) ) )
28 27 com13 
 |-  ( ( y e. B /\ ( z e. C /\ x e. A ) ) -> ( ( z -h x ) = y -> ( A C_ C -> y e. ( B i^i C ) ) ) )
29 28 ancoms 
 |-  ( ( ( z e. C /\ x e. A ) /\ y e. B ) -> ( ( z -h x ) = y -> ( A C_ C -> y e. ( B i^i C ) ) ) )
30 29 anasss 
 |-  ( ( z e. C /\ ( x e. A /\ y e. B ) ) -> ( ( z -h x ) = y -> ( A C_ C -> y e. ( B i^i C ) ) ) )
31 13 30 sylbird 
 |-  ( ( z e. C /\ ( x e. A /\ y e. B ) ) -> ( z = ( x +h y ) -> ( A C_ C -> y e. ( B i^i C ) ) ) )
32 31 imp 
 |-  ( ( ( z e. C /\ ( x e. A /\ y e. B ) ) /\ z = ( x +h y ) ) -> ( A C_ C -> y e. ( B i^i C ) ) )
33 2 3 shincli 
 |-  ( B i^i C ) e. SH
34 1 33 shsvai 
 |-  ( ( x e. A /\ y e. ( B i^i C ) ) -> ( x +h y ) e. ( A +H ( B i^i C ) ) )
35 eleq1 
 |-  ( z = ( x +h y ) -> ( z e. ( A +H ( B i^i C ) ) <-> ( x +h y ) e. ( A +H ( B i^i C ) ) ) )
36 34 35 syl5ibr 
 |-  ( z = ( x +h y ) -> ( ( x e. A /\ y e. ( B i^i C ) ) -> z e. ( A +H ( B i^i C ) ) ) )
37 36 expd 
 |-  ( z = ( x +h y ) -> ( x e. A -> ( y e. ( B i^i C ) -> z e. ( A +H ( B i^i C ) ) ) ) )
38 37 com12 
 |-  ( x e. A -> ( z = ( x +h y ) -> ( y e. ( B i^i C ) -> z e. ( A +H ( B i^i C ) ) ) ) )
39 38 ad2antrl 
 |-  ( ( z e. C /\ ( x e. A /\ y e. B ) ) -> ( z = ( x +h y ) -> ( y e. ( B i^i C ) -> z e. ( A +H ( B i^i C ) ) ) ) )
40 39 imp 
 |-  ( ( ( z e. C /\ ( x e. A /\ y e. B ) ) /\ z = ( x +h y ) ) -> ( y e. ( B i^i C ) -> z e. ( A +H ( B i^i C ) ) ) )
41 32 40 syld 
 |-  ( ( ( z e. C /\ ( x e. A /\ y e. B ) ) /\ z = ( x +h y ) ) -> ( A C_ C -> z e. ( A +H ( B i^i C ) ) ) )
42 41 exp31 
 |-  ( z e. C -> ( ( x e. A /\ y e. B ) -> ( z = ( x +h y ) -> ( A C_ C -> z e. ( A +H ( B i^i C ) ) ) ) ) )
43 42 rexlimdvv 
 |-  ( z e. C -> ( E. x e. A E. y e. B z = ( x +h y ) -> ( A C_ C -> z e. ( A +H ( B i^i C ) ) ) ) )
44 5 43 syl5bi 
 |-  ( z e. C -> ( z e. ( A +H B ) -> ( A C_ C -> z e. ( A +H ( B i^i C ) ) ) ) )
45 44 com13 
 |-  ( A C_ C -> ( z e. ( A +H B ) -> ( z e. C -> z e. ( A +H ( B i^i C ) ) ) ) )
46 45 impd 
 |-  ( A C_ C -> ( ( z e. ( A +H B ) /\ z e. C ) -> z e. ( A +H ( B i^i C ) ) ) )
47 4 46 syl5bi 
 |-  ( A C_ C -> ( z e. ( ( A +H B ) i^i C ) -> z e. ( A +H ( B i^i C ) ) ) )
48 47 ssrdv 
 |-  ( A C_ C -> ( ( A +H B ) i^i C ) C_ ( A +H ( B i^i C ) ) )