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

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 ( 𝐻 ∈ Sℋ → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp )

Proof

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