Metamath Proof Explorer

Theorem hhssablo

Description: Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

Ref Expression
Assertion hhssablo ⊢ H ∈ S ℋ → + ℎ ↾ H × H ∈ AbelOp

Proof

Step Hyp Ref Expression
1 xpeq1 ⊢ H = if H ∈ S ℋ H ℋ → H × H = if H ∈ S ℋ H ℋ × H
2 xpeq2 ⊢ H = if H ∈ S ℋ H ℋ → if H ∈ S ℋ H ℋ × H = if H ∈ S ℋ H ℋ × if H ∈ S ℋ H ℋ
3 1 2 eqtrd ⊢ H = if H ∈ S ℋ H ℋ → H × H = if H ∈ S ℋ H ℋ × if H ∈ S ℋ H ℋ
4 3 reseq2d ⊢ H = if H ∈ S ℋ H ℋ → + ℎ ↾ H × H = + ℎ ↾ if H ∈ S ℋ H ℋ × if H ∈ S ℋ H ℋ
5 4 eleq1d ⊢ H = if H ∈ S ℋ H ℋ → + ℎ ↾ H × H ∈ AbelOp ↔ + ℎ ↾ if H ∈ S ℋ H ℋ × if H ∈ S ℋ H ℋ ∈ AbelOp
6 helsh ⊢ ℋ ∈ S ℋ
7 6 elimel ⊢ if H ∈ S ℋ H ℋ ∈ S ℋ
8 7 hhssabloi ⊢ + ℎ ↾ if H ∈ S ℋ H ℋ × if H ∈ S ℋ H ℋ ∈ AbelOp
9 5 8 dedth ⊢ H ∈ S ℋ → + ℎ ↾ H × H ∈ AbelOp