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

Metamath Proof Explorer

Theorem shslej

Description: Subspace sum is smaller than subspace join. Remark in Kalmbach p. 65. (Contributed by NM, 12-Jul-2004) (New usage is discouraged.)

Ref Expression
Assertion shslej ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ 𝐵 ) )
2 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ 𝐵 ) )
3 1 2 sseq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) → ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ 𝐵 ) ⊆ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ 𝐵 ) ) )
4 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ 𝐵 ) = ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) )
5 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ 𝐵 ) = ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) )
6 4 5 sseq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) → ( ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ 𝐵 ) ⊆ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ 𝐵 ) ↔ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) ⊆ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) ) )
7 helsh ⊢ ℋ ∈ Sℋ
8 7 elimel ⊢ if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∈ Sℋ
9 7 elimel ⊢ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ∈ Sℋ
10 8 9 shsleji ⊢ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) +ℋ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) ⊆ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∨ℋ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) )
11 3 6 10 dedth2h ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )