cphsscph

Description: A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008) (Revised by AV, 25-Sep-2022)

	Ref	Expression
Hypotheses	cphsscph.x	$⊢ X = W ↾_{𝑠} U$
	cphsscph.s	$⊢ S = LSubSp (W)$
Assertion	cphsscph	$⊢ (W \in CPreHil \land U \in S) \to X \in CPreHil$

Proof

Step	Hyp	Ref	Expression
1		cphsscph.x	$⊢ X = W ↾_{𝑠} U$
2		cphsscph.s	$⊢ S = LSubSp (W)$
3		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
4	1 2	phlssphl	$⊢ (W \in PreHil \land U \in S) \to X \in PreHil$
5	3 4	sylan	$⊢ (W \in CPreHil \land U \in S) \to X \in PreHil$
6		cphnlm	$⊢ W \in CPreHil \to W \in NrmMod$
7	1 2	lssnlm	$⊢ (W \in NrmMod \land U \in S) \to X \in NrmMod$
8	6 7	sylan	$⊢ (W \in CPreHil \land U \in S) \to X \in NrmMod$
9		eqid	$⊢ Scalar (W) = Scalar (W)$
10		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
11	9 10	cphsca	$⊢ W \in CPreHil \to Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)}$
12	11	adantr	$⊢ (W \in CPreHil \land U \in S) \to Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)}$
13	1 9	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
14	13	fveq2d	$⊢ U \in S \to {Base}_{Scalar (W)} = {Base}_{Scalar (X)}$
15	14	oveq2d	$⊢ U \in S \to ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)} = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (X)}$
16	13 15	eqeq12d	$⊢ U \in S \to (Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)} \leftrightarrow Scalar (X) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (X)})$
17	16	adantl	$⊢ (W \in CPreHil \land U \in S) \to (Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)} \leftrightarrow Scalar (X) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (X)})$
18	12 17	mpbid	$⊢ (W \in CPreHil \land U \in S) \to Scalar (X) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (X)}$
19	5 8 18	3jca	$⊢ (W \in CPreHil \land U \in S) \to (X \in PreHil \land X \in NrmMod \land Scalar (X) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (X)})$
20		simpl	$⊢ (W \in CPreHil \land U \in S) \to W \in CPreHil$
21		elinel1	$⊢ q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \to q \in {Base}_{Scalar (W)}$
22	21	adantr	$⊢ (q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \to q \in {Base}_{Scalar (W)}$
23		elinel2	$⊢ q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \to q \in [0, +∞)$
24		elrege0	$⊢ q \in [0, +∞) \leftrightarrow (q \in ℝ \land 0 \leq q)$
25	24	simplbi	$⊢ q \in [0, +∞) \to q \in ℝ$
26	23 25	syl	$⊢ q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \to q \in ℝ$
27	26	adantr	$⊢ (q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \to q \in ℝ$
28	24	simprbi	$⊢ q \in [0, +∞) \to 0 \leq q$
29	23 28	syl	$⊢ q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \to 0 \leq q$
30	29	adantr	$⊢ (q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \to 0 \leq q$
31	22 27 30	3jca	$⊢ (q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \to (q \in {Base}_{Scalar (W)} \land q \in ℝ \land 0 \leq q)$
32	9 10	cphsqrtcl	$⊢ (W \in CPreHil \land (q \in {Base}_{Scalar (W)} \land q \in ℝ \land 0 \leq q)) \to \sqrt{q} \in {Base}_{Scalar (W)}$
33	20 31 32	syl2anr	$⊢ ((q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \land (W \in CPreHil \land U \in S)) \to \sqrt{q} \in {Base}_{Scalar (W)}$
34		eleq1	$⊢ \sqrt{q} = x \to (\sqrt{q} \in {Base}_{Scalar (W)} \leftrightarrow x \in {Base}_{Scalar (W)})$
35	34	adantl	$⊢ (q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \to (\sqrt{q} \in {Base}_{Scalar (W)} \leftrightarrow x \in {Base}_{Scalar (W)})$
36	35	adantr	$⊢ ((q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \land (W \in CPreHil \land U \in S)) \to (\sqrt{q} \in {Base}_{Scalar (W)} \leftrightarrow x \in {Base}_{Scalar (W)})$
37	33 36	mpbid	$⊢ ((q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \land (W \in CPreHil \land U \in S)) \to x \in {Base}_{Scalar (W)}$
38	37	ex	$⊢ (q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \land \sqrt{q} = x) \to ((W \in CPreHil \land U \in S) \to x \in {Base}_{Scalar (W)})$
39	38	rexlimiva	$⊢ \exists q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \sqrt{q} = x \to ((W \in CPreHil \land U \in S) \to x \in {Base}_{Scalar (W)})$
40		df-sqrt	$⊢ \sqrt = (x \in ℂ ⟼ (ι c \in ℂ \| (c^{2} = x \land 0 \leq ℜ (c) \land i c \notin ℝ^{+})))$
41	40	funmpt2	$⊢ Fun \sqrt$
42		fvelima	$⊢ (Fun \sqrt \land x \in \sqrt [{Base}_{Scalar (W)} \cap [0, +∞)]) \to \exists q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \sqrt{q} = x$
43	41 42	mpan	$⊢ x \in \sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] \to \exists q \in ({Base}_{Scalar (W)} \cap [0, +∞)) \sqrt{q} = x$
44	39 43	syl11	$⊢ (W \in CPreHil \land U \in S) \to (x \in \sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] \to x \in {Base}_{Scalar (W)})$
45	44	ssrdv	$⊢ (W \in CPreHil \land U \in S) \to \sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] \subseteq {Base}_{Scalar (W)}$
46	14	ineq1d	$⊢ U \in S \to {Base}_{Scalar (W)} \cap [0, +∞) = {Base}_{Scalar (X)} \cap [0, +∞)$
47	46	imaeq2d	$⊢ U \in S \to \sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] = \sqrt [{Base}_{Scalar (X)} \cap [0, +∞)]$
48	47 14	sseq12d	$⊢ U \in S \to (\sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] \subseteq {Base}_{Scalar (W)} \leftrightarrow \sqrt [{Base}_{Scalar (X)} \cap [0, +∞)] \subseteq {Base}_{Scalar (X)})$
49	48	adantl	$⊢ (W \in CPreHil \land U \in S) \to (\sqrt [{Base}_{Scalar (W)} \cap [0, +∞)] \subseteq {Base}_{Scalar (W)} \leftrightarrow \sqrt [{Base}_{Scalar (X)} \cap [0, +∞)] \subseteq {Base}_{Scalar (X)})$
50	45 49	mpbid	$⊢ (W \in CPreHil \land U \in S) \to \sqrt [{Base}_{Scalar (X)} \cap [0, +∞)] \subseteq {Base}_{Scalar (X)}$
51		cphlmod	$⊢ W \in CPreHil \to W \in LMod$
52	2	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
53	51 52	sylan	$⊢ (W \in CPreHil \land U \in S) \to U \in SubGrp (W)$
54		eqid	$⊢ norm (W) = norm (W)$
55		eqid	$⊢ norm (X) = norm (X)$
56	1 54 55	subgnm	$⊢ U \in SubGrp (W) \to norm (X) = {norm (W) ↾}_{U}$
57	53 56	syl	$⊢ (W \in CPreHil \land U \in S) \to norm (X) = {norm (W) ↾}_{U}$
58		eqid	$⊢ {Base}_{W} = {Base}_{W}$
59		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
60	58 59 54	cphnmfval	$⊢ W \in CPreHil \to norm (W) = (b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (W) b})$
61	60	adantr	$⊢ (W \in CPreHil \land U \in S) \to norm (W) = (b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (W) b})$
62	1 59	ressip	$⊢ U \in S \to \cdot_{𝑖} (W) = \cdot_{𝑖} (X)$
63	62	adantl	$⊢ (W \in CPreHil \land U \in S) \to \cdot_{𝑖} (W) = \cdot_{𝑖} (X)$
64	63	oveqd	$⊢ (W \in CPreHil \land U \in S) \to b \cdot_{𝑖} (W) b = b \cdot_{𝑖} (X) b$
65	64	fveq2d	$⊢ (W \in CPreHil \land U \in S) \to \sqrt{b \cdot_{𝑖} (W) b} = \sqrt{b \cdot_{𝑖} (X) b}$
66	65	mpteq2dv	$⊢ (W \in CPreHil \land U \in S) \to (b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (W) b}) = (b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b})$
67	61 66	eqtrd	$⊢ (W \in CPreHil \land U \in S) \to norm (W) = (b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b})$
68	58 2	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
69	68	adantl	$⊢ (W \in CPreHil \land U \in S) \to U \subseteq {Base}_{W}$
70		dfss	$⊢ U \subseteq {Base}_{W} \leftrightarrow U = U \cap {Base}_{W}$
71	69 70	sylib	$⊢ (W \in CPreHil \land U \in S) \to U = U \cap {Base}_{W}$
72	67 71	reseq12d	$⊢ (W \in CPreHil \land U \in S) \to {norm (W) ↾}_{U} = {(b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b}) ↾}_{(U \cap {Base}_{W})}$
73	1 58	ressbas	$⊢ U \in S \to U \cap {Base}_{W} = {Base}_{X}$
74	73	adantl	$⊢ (W \in CPreHil \land U \in S) \to U \cap {Base}_{W} = {Base}_{X}$
75	74	reseq2d	$⊢ (W \in CPreHil \land U \in S) \to {(b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b}) ↾}_{(U \cap {Base}_{W})} = {(b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b}) ↾}_{{Base}_{X}}$
76	72 75	eqtrd	$⊢ (W \in CPreHil \land U \in S) \to {norm (W) ↾}_{U} = {(b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b}) ↾}_{{Base}_{X}}$
77	1 58	ressbasss	$⊢ {Base}_{X} \subseteq {Base}_{W}$
78	77	a1i	$⊢ (W \in CPreHil \land U \in S) \to {Base}_{X} \subseteq {Base}_{W}$
79	78	resmptd	$⊢ (W \in CPreHil \land U \in S) \to {(b \in {Base}_{W} ⟼ \sqrt{b \cdot_{𝑖} (X) b}) ↾}_{{Base}_{X}} = (b \in {Base}_{X} ⟼ \sqrt{b \cdot_{𝑖} (X) b})$
80	57 76 79	3eqtrd	$⊢ (W \in CPreHil \land U \in S) \to norm (X) = (b \in {Base}_{X} ⟼ \sqrt{b \cdot_{𝑖} (X) b})$
81		eqid	$⊢ {Base}_{X} = {Base}_{X}$
82		eqid	$⊢ \cdot_{𝑖} (X) = \cdot_{𝑖} (X)$
83		eqid	$⊢ Scalar (X) = Scalar (X)$
84		eqid	$⊢ {Base}_{Scalar (X)} = {Base}_{Scalar (X)}$
85	81 82 55 83 84	iscph	$⊢ X \in CPreHil \leftrightarrow ((X \in PreHil \land X \in NrmMod \land Scalar (X) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (X)}) \land \sqrt [{Base}_{Scalar (X)} \cap [0, +∞)] \subseteq {Base}_{Scalar (X)} \land norm (X) = (b \in {Base}_{X} ⟼ \sqrt{b \cdot_{𝑖} (X) b}))$
86	19 50 80 85	syl3anbrc	$⊢ (W \in CPreHil \land U \in S) \to X \in CPreHil$

Metamath Proof Explorer

Theorem cphsscph

Proof