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