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 ) |