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	⊢ 𝐴 ∈ Sℋ
	shmod.2	⊢ 𝐵 ∈ Sℋ
	shmod.3	⊢ 𝐶 ∈ Sℋ
Assertion	shmodi	⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		shmod.1	⊢ 𝐴 ∈ Sℋ
2		shmod.2	⊢ 𝐵 ∈ Sℋ
3		shmod.3	⊢ 𝐶 ∈ Sℋ
4	1 2 3	shmodsi	⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) )
5		ineq1	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) )
6	5	sseq1d	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
7	4 6	syl5ib	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
8	7	imp	⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) )
9	2 3	shincli	⊢ ( 𝐵 ∩ 𝐶 ) ∈ Sℋ
10	1 9	shsleji	⊢ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) )
11	8 10	sstrdi	⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) )