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ℋ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )