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