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