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