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 ⊢ 𝐴 ∈ 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 imbitrid ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
8 7 imp ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) )
9 2 3 shincli ⊢ ( 𝐵 ∩ 𝐶 ) ∈ Sℋ
10 1 9 shsleji ⊢ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) )
11 8 10 sstrdi ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) )