hhshsslem1

Description: Lemma for hhsssh . (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsst.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	hhsst.2	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
	hhssp3.3	$⊢ W \in SubSp (U)$
	hhssp3.4	$⊢ H \subseteq ℋ$
Assertion	hhshsslem1	$⊢ H = BaseSet (W)$

Proof

Step	Hyp	Ref	Expression
1		hhsst.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2		hhsst.2	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
3		hhssp3.3	$⊢ W \in SubSp (U)$
4		hhssp3.4	$⊢ H \subseteq ℋ$
5		eqid	$⊢ BaseSet (W) = BaseSet (W)$
6		eqid	$⊢ +_{v} (W) = +_{v} (W)$
7	5 6	bafval	$⊢ BaseSet (W) = ran +_{v} (W)$
8	1	hhnv	$⊢ U \in NrmCVec$
9		eqid	$⊢ SubSp (U) = SubSp (U)$
10	9	sspnv	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to W \in NrmCVec$
11	8 3 10	mp2an	$⊢ W \in NrmCVec$
12	6	nvgrp	$⊢ W \in NrmCVec \to +_{v} (W) \in GrpOp$
13		grporndm	$⊢ +_{v} (W) \in GrpOp \to ran +_{v} (W) = dom dom +_{v} (W)$
14	11 12 13	mp2b	$⊢ ran +_{v} (W) = dom dom +_{v} (W)$
15	2	fveq2i	$⊢ +_{v} (W) = +_{v} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩)$
16		eqid	$⊢ +_{v} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩) = +_{v} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩)$
17	16	vafval	$⊢ +_{v} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩) = 1^{st} (1^{st} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩))$
18		opex	$⊢ ⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩ \in V$
19		normf	$⊢ {norm}_{ℎ} : ℋ ⟶ ℝ$
20		ax-hilex	$⊢ ℋ \in V$
21		fex	$⊢ ({norm}_{ℎ} : ℋ ⟶ ℝ \land ℋ \in V) \to {norm}_{ℎ} \in V$
22	19 20 21	mp2an	$⊢ {norm}_{ℎ} \in V$
23	22	resex	$⊢ {{norm}_{ℎ} ↾}_{H} \in V$
24	18 23	op1st	$⊢ 1^{st} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩) = ⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩$
25	24	fveq2i	$⊢ 1^{st} (1^{st} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩)) = 1^{st} (⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩)$
26		hilablo	$⊢ +_{ℎ} \in AbelOp$
27		resexg	$⊢ +_{ℎ} \in AbelOp \to {+_{ℎ} ↾}_{(H \times H)} \in V$
28	26 27	ax-mp	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in V$
29		hvmulex	$⊢ \cdot_{ℎ} \in V$
30	29	resex	$⊢ {\cdot_{ℎ} ↾}_{(ℂ \times H)} \in V$
31	28 30	op1st	$⊢ 1^{st} (⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩) = {+_{ℎ} ↾}_{(H \times H)}$
32	25 31	eqtri	$⊢ 1^{st} (1^{st} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩)) = {+_{ℎ} ↾}_{(H \times H)}$
33	17 32	eqtri	$⊢ +_{v} (⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩) = {+_{ℎ} ↾}_{(H \times H)}$
34	15 33	eqtri	$⊢ +_{v} (W) = {+_{ℎ} ↾}_{(H \times H)}$
35	34	dmeqi	$⊢ dom +_{v} (W) = dom ({+_{ℎ} ↾}_{(H \times H)})$
36		xpss12	$⊢ (H \subseteq ℋ \land H \subseteq ℋ) \to H \times H \subseteq ℋ \times ℋ$
37	4 4 36	mp2an	$⊢ H \times H \subseteq ℋ \times ℋ$
38		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
39	38	fdmi	$⊢ dom +_{ℎ} = ℋ \times ℋ$
40	37 39	sseqtrri	$⊢ H \times H \subseteq dom +_{ℎ}$
41		ssdmres	$⊢ H \times H \subseteq dom +_{ℎ} \leftrightarrow dom ({+_{ℎ} ↾}_{(H \times H)}) = H \times H$
42	40 41	mpbi	$⊢ dom ({+_{ℎ} ↾}_{(H \times H)}) = H \times H$
43	35 42	eqtri	$⊢ dom +_{v} (W) = H \times H$
44	43	dmeqi	$⊢ dom dom +_{v} (W) = dom (H \times H)$
45		dmxpid	$⊢ dom (H \times H) = H$
46	44 45	eqtri	$⊢ dom dom +_{v} (W) = H$
47	14 46	eqtri	$⊢ ran +_{v} (W) = H$
48	7 47	eqtri	$⊢ BaseSet (W) = H$
49	48	eqcomi	$⊢ H = BaseSet (W)$

Metamath Proof Explorer

Theorem hhshsslem1

Proof