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 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A + ℋ B ⊆ A ∨ ℋ B

Proof

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