hhssabloilem

Description: Lemma for hhssabloi . Formerly part of proof for hhssabloi which was based on the deprecated definition "SubGrpOp" for subgroups. (Contributed by NM, 9-Apr-2008) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 27-Aug-2021) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	hhssabl.1	$⊢ H \in S_{ℋ}$
	Assertion	hhssabloilem	$⊢ (+_{ℎ} \in GrpOp \land {+_{ℎ} ↾}_{(H \times H)} \in GrpOp \land {+_{ℎ} ↾}_{(H \times H)} \subseteq +_{ℎ})$

Proof

Step	Hyp	Ref	Expression
1		hhssabl.1	$⊢ H \in S_{ℋ}$
2		hilablo	$⊢ +_{ℎ} \in AbelOp$
3		ablogrpo	$⊢ +_{ℎ} \in AbelOp \to +_{ℎ} \in GrpOp$
4	2 3	ax-mp	$⊢ +_{ℎ} \in GrpOp$
5	1	elexi	$⊢ H \in V$
6		eqid	$⊢ ran +_{ℎ} = ran +_{ℎ}$
7	6	grpofo	$⊢ +_{ℎ} \in GrpOp \to +_{ℎ} : ran +_{ℎ} \times ran +_{ℎ} \underset{onto}{⟶} ran +_{ℎ}$
8		fof	$⊢ +_{ℎ} : ran +_{ℎ} \times ran +_{ℎ} \underset{onto}{⟶} ran +_{ℎ} \to +_{ℎ} : ran +_{ℎ} \times ran +_{ℎ} ⟶ ran +_{ℎ}$
9	4 7 8	mp2b	$⊢ +_{ℎ} : ran +_{ℎ} \times ran +_{ℎ} ⟶ ran +_{ℎ}$
10	1	shssii	$⊢ H \subseteq ℋ$
11		df-hba	$⊢ ℋ = BaseSet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
12		eqid	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
13	12	hhva	$⊢ +_{ℎ} = +_{v} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
14	11 13	bafval	$⊢ ℋ = ran +_{ℎ}$
15	10 14	sseqtri	$⊢ H \subseteq ran +_{ℎ}$
16		xpss12	$⊢ (H \subseteq ran +_{ℎ} \land H \subseteq ran +_{ℎ}) \to H \times H \subseteq ran +_{ℎ} \times ran +_{ℎ}$
17	15 15 16	mp2an	$⊢ H \times H \subseteq ran +_{ℎ} \times ran +_{ℎ}$
18		fssres	$⊢ (+_{ℎ} : ran +_{ℎ} \times ran +_{ℎ} ⟶ ran +_{ℎ} \land H \times H \subseteq ran +_{ℎ} \times ran +_{ℎ}) \to ({+_{ℎ} ↾}_{(H \times H)}) : H \times H ⟶ ran +_{ℎ}$
19	9 17 18	mp2an	$⊢ ({+_{ℎ} ↾}_{(H \times H)}) : H \times H ⟶ ran +_{ℎ}$
20		ffn	$⊢ ({+_{ℎ} ↾}_{(H \times H)}) : H \times H ⟶ ran +_{ℎ} \to ({+_{ℎ} ↾}_{(H \times H)}) Fn (H \times H)$
21	19 20	ax-mp	$⊢ ({+_{ℎ} ↾}_{(H \times H)}) Fn (H \times H)$
22		ovres	$⊢ (x \in H \land y \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) y = x +_{ℎ} y$
23		shaddcl	$⊢ (H \in S_{ℋ} \land x \in H \land y \in H) \to x +_{ℎ} y \in H$
24	1 23	mp3an1	$⊢ (x \in H \land y \in H) \to x +_{ℎ} y \in H$
25	22 24	eqeltrd	$⊢ (x \in H \land y \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) y \in H$
26	25	rgen2	$⊢ \forall x \in H \forall y \in H x ({+_{ℎ} ↾}_{(H \times H)}) y \in H$
27		ffnov	$⊢ ({+_{ℎ} ↾}_{(H \times H)}) : H \times H ⟶ H \leftrightarrow (({+_{ℎ} ↾}_{(H \times H)}) Fn (H \times H) \land \forall x \in H \forall y \in H x ({+_{ℎ} ↾}_{(H \times H)}) y \in H)$
28	21 26 27	mpbir2an	$⊢ ({+_{ℎ} ↾}_{(H \times H)}) : H \times H ⟶ H$
29	22	oveq1d	$⊢ (x \in H \land y \in H) \to (x ({+_{ℎ} ↾}_{(H \times H)}) y) +_{ℎ} z = (x +_{ℎ} y) +_{ℎ} z$
30	29	3adant3	$⊢ (x \in H \land y \in H \land z \in H) \to (x ({+_{ℎ} ↾}_{(H \times H)}) y) +_{ℎ} z = (x +_{ℎ} y) +_{ℎ} z$
31		ovres	$⊢ (x ({+_{ℎ} ↾}_{(H \times H)}) y \in H \land z \in H) \to (x ({+_{ℎ} ↾}_{(H \times H)}) y) ({+_{ℎ} ↾}_{(H \times H)}) z = (x ({+_{ℎ} ↾}_{(H \times H)}) y) +_{ℎ} z$
32	25 31	stoic3	$⊢ (x \in H \land y \in H \land z \in H) \to (x ({+_{ℎ} ↾}_{(H \times H)}) y) ({+_{ℎ} ↾}_{(H \times H)}) z = (x ({+_{ℎ} ↾}_{(H \times H)}) y) +_{ℎ} z$
33		ovres	$⊢ (y \in H \land z \in H) \to y ({+_{ℎ} ↾}_{(H \times H)}) z = y +_{ℎ} z$
34	33	oveq2d	$⊢ (y \in H \land z \in H) \to x +_{ℎ} (y ({+_{ℎ} ↾}_{(H \times H)}) z) = x +_{ℎ} (y +_{ℎ} z)$
35	34	3adant1	$⊢ (x \in H \land y \in H \land z \in H) \to x +_{ℎ} (y ({+_{ℎ} ↾}_{(H \times H)}) z) = x +_{ℎ} (y +_{ℎ} z)$
36	28	fovcl	$⊢ (y \in H \land z \in H) \to y ({+_{ℎ} ↾}_{(H \times H)}) z \in H$
37		ovres	$⊢ (x \in H \land y ({+_{ℎ} ↾}_{(H \times H)}) z \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) (y ({+_{ℎ} ↾}_{(H \times H)}) z) = x +_{ℎ} (y ({+_{ℎ} ↾}_{(H \times H)}) z)$
38	36 37	sylan2	$⊢ (x \in H \land (y \in H \land z \in H)) \to x ({+_{ℎ} ↾}_{(H \times H)}) (y ({+_{ℎ} ↾}_{(H \times H)}) z) = x +_{ℎ} (y ({+_{ℎ} ↾}_{(H \times H)}) z)$
39	38	3impb	$⊢ (x \in H \land y \in H \land z \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) (y ({+_{ℎ} ↾}_{(H \times H)}) z) = x +_{ℎ} (y ({+_{ℎ} ↾}_{(H \times H)}) z)$
40	15	sseli	$⊢ x \in H \to x \in ran +_{ℎ}$
41	15	sseli	$⊢ y \in H \to y \in ran +_{ℎ}$
42	15	sseli	$⊢ z \in H \to z \in ran +_{ℎ}$
43	6	grpoass	$⊢ (+_{ℎ} \in GrpOp \land (x \in ran +_{ℎ} \land y \in ran +_{ℎ} \land z \in ran +_{ℎ})) \to (x +_{ℎ} y) +_{ℎ} z = x +_{ℎ} (y +_{ℎ} z)$
44	4 43	mpan	$⊢ (x \in ran +_{ℎ} \land y \in ran +_{ℎ} \land z \in ran +_{ℎ}) \to (x +_{ℎ} y) +_{ℎ} z = x +_{ℎ} (y +_{ℎ} z)$
45	40 41 42 44	syl3an	$⊢ (x \in H \land y \in H \land z \in H) \to (x +_{ℎ} y) +_{ℎ} z = x +_{ℎ} (y +_{ℎ} z)$
46	35 39 45	3eqtr4d	$⊢ (x \in H \land y \in H \land z \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) (y ({+_{ℎ} ↾}_{(H \times H)}) z) = (x +_{ℎ} y) +_{ℎ} z$
47	30 32 46	3eqtr4d	$⊢ (x \in H \land y \in H \land z \in H) \to (x ({+_{ℎ} ↾}_{(H \times H)}) y) ({+_{ℎ} ↾}_{(H \times H)}) z = x ({+_{ℎ} ↾}_{(H \times H)}) (y ({+_{ℎ} ↾}_{(H \times H)}) z)$
48		hilid	$⊢ GId (+_{ℎ}) = 0_{ℎ}$
49		sh0	$⊢ H \in S_{ℋ} \to 0_{ℎ} \in H$
50	1 49	ax-mp	$⊢ 0_{ℎ} \in H$
51	48 50	eqeltri	$⊢ GId (+_{ℎ}) \in H$
52		ovres	$⊢ (GId (+_{ℎ}) \in H \land x \in H) \to GId (+_{ℎ}) ({+_{ℎ} ↾}_{(H \times H)}) x = GId (+_{ℎ}) +_{ℎ} x$
53	51 52	mpan	$⊢ x \in H \to GId (+_{ℎ}) ({+_{ℎ} ↾}_{(H \times H)}) x = GId (+_{ℎ}) +_{ℎ} x$
54		eqid	$⊢ GId (+_{ℎ}) = GId (+_{ℎ})$
55	6 54	grpolid	$⊢ (+_{ℎ} \in GrpOp \land x \in ran +_{ℎ}) \to GId (+_{ℎ}) +_{ℎ} x = x$
56	4 40 55	sylancr	$⊢ x \in H \to GId (+_{ℎ}) +_{ℎ} x = x$
57	53 56	eqtrd	$⊢ x \in H \to GId (+_{ℎ}) ({+_{ℎ} ↾}_{(H \times H)}) x = x$
58	12	hhnv	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ \in NrmCVec$
59	12	hhsm	$⊢ \cdot_{ℎ} = \cdot_{𝑠OLD} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
60		eqid	$⊢ \cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1} = \cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1}$
61	13 59 60	nvinvfval	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ \in NrmCVec \to \cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1} = inv (+_{ℎ})$
62	58 61	ax-mp	$⊢ \cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1} = inv (+_{ℎ})$
63	62	eqcomi	$⊢ inv (+_{ℎ}) = \cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1}$
64	63	fveq1i	$⊢ inv (+_{ℎ}) (x) = (\cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1}) (x)$
65		ax-hfvmul	$⊢ \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ$
66		ffn	$⊢ \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ \to \cdot_{ℎ} Fn (ℂ \times ℋ)$
67	65 66	ax-mp	$⊢ \cdot_{ℎ} Fn (ℂ \times ℋ)$
68		neg1cn	$⊢ - 1 \in ℂ$
69	60	curry1val	$⊢ (\cdot_{ℎ} Fn (ℂ \times ℋ) \land - 1 \in ℂ) \to (\cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1}) (x) = -1 \cdot_{ℎ} x$
70	67 68 69	mp2an	$⊢ (\cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1}) (x) = -1 \cdot_{ℎ} x$
71		shmulcl	$⊢ (H \in S_{ℋ} \land - 1 \in ℂ \land x \in H) \to -1 \cdot_{ℎ} x \in H$
72	1 68 71	mp3an12	$⊢ x \in H \to -1 \cdot_{ℎ} x \in H$
73	70 72	eqeltrid	$⊢ x \in H \to (\cdot_{ℎ} \circ {({2^{nd} ↾}_{(\{- 1\} \times V)})}^{-1}) (x) \in H$
74	64 73	eqeltrid	$⊢ x \in H \to inv (+_{ℎ}) (x) \in H$
75		ovres	$⊢ (inv (+_{ℎ}) (x) \in H \land x \in H) \to inv (+_{ℎ}) (x) ({+_{ℎ} ↾}_{(H \times H)}) x = inv (+_{ℎ}) (x) +_{ℎ} x$
76	74 75	mpancom	$⊢ x \in H \to inv (+_{ℎ}) (x) ({+_{ℎ} ↾}_{(H \times H)}) x = inv (+_{ℎ}) (x) +_{ℎ} x$
77		eqid	$⊢ inv (+_{ℎ}) = inv (+_{ℎ})$
78	6 54 77	grpolinv	$⊢ (+_{ℎ} \in GrpOp \land x \in ran +_{ℎ}) \to inv (+_{ℎ}) (x) +_{ℎ} x = GId (+_{ℎ})$
79	4 40 78	sylancr	$⊢ x \in H \to inv (+_{ℎ}) (x) +_{ℎ} x = GId (+_{ℎ})$
80	76 79	eqtrd	$⊢ x \in H \to inv (+_{ℎ}) (x) ({+_{ℎ} ↾}_{(H \times H)}) x = GId (+_{ℎ})$
81	5 28 47 51 57 74 80	isgrpoi	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in GrpOp$
82		resss	$⊢ {+_{ℎ} ↾}_{(H \times H)} \subseteq +_{ℎ}$
83	4 81 82	3pm3.2i	$⊢ (+_{ℎ} \in GrpOp \land {+_{ℎ} ↾}_{(H \times H)} \in GrpOp \land {+_{ℎ} ↾}_{(H \times H)} \subseteq +_{ℎ})$

Metamath Proof Explorer

Theorem hhssabloilem

Proof