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	$⊢ H \in S_{ℋ}$
	Assertion	hhssabloi	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in AbelOp$

Proof

Step	Hyp	Ref	Expression
1		hhssabl.1	$⊢ H \in S_{ℋ}$
2	1	hhssabloilem	$⊢ (+_{ℎ} \in GrpOp \land {+_{ℎ} ↾}_{(H \times H)} \in GrpOp \land {+_{ℎ} ↾}_{(H \times H)} \subseteq +_{ℎ})$
3	2	simp2i	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in GrpOp$
4	1	shssii	$⊢ H \subseteq ℋ$
5		xpss12	$⊢ (H \subseteq ℋ \land H \subseteq ℋ) \to H \times H \subseteq ℋ \times ℋ$
6	4 4 5	mp2an	$⊢ H \times H \subseteq ℋ \times ℋ$
7		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
8	7	fdmi	$⊢ dom +_{ℎ} = ℋ \times ℋ$
9	6 8	sseqtrri	$⊢ H \times H \subseteq dom +_{ℎ}$
10		ssdmres	$⊢ H \times H \subseteq dom +_{ℎ} \leftrightarrow dom ({+_{ℎ} ↾}_{(H \times H)}) = H \times H$
11	9 10	mpbi	$⊢ dom ({+_{ℎ} ↾}_{(H \times H)}) = H \times H$
12	1	sheli	$⊢ x \in H \to x \in ℋ$
13	1	sheli	$⊢ y \in H \to y \in ℋ$
14		ax-hvcom	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} y = y +_{ℎ} x$
15	12 13 14	syl2an	$⊢ (x \in H \land y \in H) \to x +_{ℎ} y = y +_{ℎ} x$
16		ovres	$⊢ (x \in H \land y \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) y = x +_{ℎ} y$
17		ovres	$⊢ (y \in H \land x \in H) \to y ({+_{ℎ} ↾}_{(H \times H)}) x = y +_{ℎ} x$
18	17	ancoms	$⊢ (x \in H \land y \in H) \to y ({+_{ℎ} ↾}_{(H \times H)}) x = y +_{ℎ} x$
19	15 16 18	3eqtr4d	$⊢ (x \in H \land y \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) y = y ({+_{ℎ} ↾}_{(H \times H)}) x$
20	3 11 19	isabloi	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in AbelOp$

Metamath Proof Explorer

Theorem hhssabloi

Proof