This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shmodi

Description: The modular law is implied by the closure of subspace sum. Part of proof 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 shmodi 
|- ( ( ( A +H B ) = ( A vH B ) /\ A C_ C ) -> ( ( A vH B ) i^i C ) C_ ( A vH ( 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 1 2 3 shmodsi 
 |-  ( A C_ C -> ( ( A +H B ) i^i C ) C_ ( A +H ( B i^i C ) ) )
5 ineq1 
 |-  ( ( A +H B ) = ( A vH B ) -> ( ( A +H B ) i^i C ) = ( ( A vH B ) i^i C ) )
6 5 sseq1d 
 |-  ( ( A +H B ) = ( A vH B ) -> ( ( ( A +H B ) i^i C ) C_ ( A +H ( B i^i C ) ) <-> ( ( A vH B ) i^i C ) C_ ( A +H ( B i^i C ) ) ) )
7 4 6 imbitrid 
 |-  ( ( A +H B ) = ( A vH B ) -> ( A C_ C -> ( ( A vH B ) i^i C ) C_ ( A +H ( B i^i C ) ) ) )
8 7 imp 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ A C_ C ) -> ( ( A vH B ) i^i C ) C_ ( A +H ( B i^i C ) ) )
9 2 3 shincli 
 |-  ( B i^i C ) e. SH
10 1 9 shsleji 
 |-  ( A +H ( B i^i C ) ) C_ ( A vH ( B i^i C ) )
11 8 10 sstrdi 
 |-  ( ( ( A +H B ) = ( A vH B ) /\ A C_ C ) -> ( ( A vH B ) i^i C ) C_ ( A vH ( B i^i C ) ) )