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

Metamath Proof Explorer

Theorem hhssabloi

Description: Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008) (Revised by Mario Carneiro, 23-Dec-2013) (Proof shortened by AV, 27-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis hhssabl.1 ⊢ 𝐻 ∈ Sℋ
Assertion hhssabloi ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp

Proof

Step Hyp Ref Expression
1 hhssabl.1 ⊢ 𝐻 ∈ Sℋ
2 1 hhssabloilem ⊢ ( +ℎ ∈ GrpOp ∧ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp ∧ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ )
3 2 simp2i ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp
4 1 shssii ⊢ 𝐻 ⊆ ℋ
5 xpss12 ⊢ ( ( 𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ ) → ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ ) )
6 4 4 5 mp2an ⊢ ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ )
7 ax-hfvadd ⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
8 7 fdmi ⊢ dom +ℎ = ( ℋ × ℋ )
9 6 8 sseqtrri ⊢ ( 𝐻 × 𝐻 ) ⊆ dom +ℎ
10 ssdmres ⊢ ( ( 𝐻 × 𝐻 ) ⊆ dom +ℎ ↔ dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( 𝐻 × 𝐻 ) )
11 9 10 mpbi ⊢ dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( 𝐻 × 𝐻 )
12 1 sheli ⊢ ( 𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ )
13 1 sheli ⊢ ( 𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ )
14 ax-hvcom ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
15 12 13 14 syl2an ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
16 ovres ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) )
17 ovres ⊢ ( ( 𝑦 ∈ 𝐻 ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( 𝑦 +ℎ 𝑥 ) )
18 17 ancoms ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( 𝑦 +ℎ 𝑥 ) )
19 15 16 18 3eqtr4d ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) = ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) )
20 3 11 19 isabloi ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp