phlssphl

Description: A subspace of an inner product space (pre-Hilbert space) is an inner product space. (Contributed by AV, 25-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		phlssphl.x	$⊢ X = W ↾_{𝑠} U$
2		phlssphl.s	$⊢ S = LSubSp (W)$
3		eqidd	$⊢ (W \in PreHil \land U \in S) \to {Base}_{X} = {Base}_{X}$
4		eqidd	$⊢ (W \in PreHil \land U \in S) \to +_{X} = +_{X}$
5		eqidd	$⊢ (W \in PreHil \land U \in S) \to \cdot_{X} = \cdot_{X}$
6		eqidd	$⊢ (W \in PreHil \land U \in S) \to \cdot_{𝑖} (X) = \cdot_{𝑖} (X)$
7		phllmod	$⊢ W \in PreHil \to W \in LMod$
8		eqid	$⊢ 0_{W} = 0_{W}$
9		eqid	$⊢ 0_{X} = 0_{X}$
10	1 8 9 2	lss0v	$⊢ (W \in LMod \land U \in S) \to 0_{X} = 0_{W}$
11	7 10	sylan	$⊢ (W \in PreHil \land U \in S) \to 0_{X} = 0_{W}$
12	11	eqcomd	$⊢ (W \in PreHil \land U \in S) \to 0_{W} = 0_{X}$
13		eqidd	$⊢ (W \in PreHil \land U \in S) \to Scalar (X) = Scalar (X)$
14		eqidd	$⊢ (W \in PreHil \land U \in S) \to {Base}_{Scalar (X)} = {Base}_{Scalar (X)}$
15		eqidd	$⊢ (W \in PreHil \land U \in S) \to +_{Scalar (X)} = +_{Scalar (X)}$
16		eqidd	$⊢ (W \in PreHil \land U \in S) \to \cdot_{Scalar (X)} = \cdot_{Scalar (X)}$
17		eqidd	$⊢ (W \in PreHil \land U \in S) \to _{Scalar (X)} = _{Scalar (X)}$
18		eqidd	$⊢ (W \in PreHil \land U \in S) \to 0_{Scalar (X)} = 0_{Scalar (X)}$
19		phllvec	$⊢ W \in PreHil \to W \in LVec$
20	1 2	lsslvec	$⊢ (W \in LVec \land U \in S) \to X \in LVec$
21	19 20	sylan	$⊢ (W \in PreHil \land U \in S) \to X \in LVec$
22		eqid	$⊢ Scalar (W) = Scalar (W)$
23	1 22	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
24	23	eqcomd	$⊢ U \in S \to Scalar (X) = Scalar (W)$
25	24	adantl	$⊢ (W \in PreHil \land U \in S) \to Scalar (X) = Scalar (W)$
26	22	phlsrng	$⊢ W \in PreHil \to Scalar (W) \in *-Ring$
27	26	adantr	$⊢ (W \in PreHil \land U \in S) \to Scalar (W) \in *-Ring$
28	25 27	eqeltrd	$⊢ (W \in PreHil \land U \in S) \to Scalar (X) \in *-Ring$
29		simpl	$⊢ (W \in PreHil \land U \in S) \to W \in PreHil$
30		eqid	$⊢ {Base}_{W} = {Base}_{W}$
31	1 30	ressbasss	$⊢ {Base}_{X} \subseteq {Base}_{W}$
32	31	sseli	$⊢ x \in {Base}_{X} \to x \in {Base}_{W}$
33	31	sseli	$⊢ y \in {Base}_{X} \to y \in {Base}_{W}$
34		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
35		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
36	22 34 30 35	ipcl	$⊢ (W \in PreHil \land x \in {Base}_{W} \land y \in {Base}_{W}) \to x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)}$
37	29 32 33 36	syl3an	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)}$
38	24	fveq2d	$⊢ U \in S \to {Base}_{Scalar (X)} = {Base}_{Scalar (W)}$
39	38	eleq2d	$⊢ U \in S \to (x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)})$
40	39	adantl	$⊢ (W \in PreHil \land U \in S) \to (x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)})$
41	40	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to (x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)})$
42	37 41	mpbird	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)}$
43		eqid	$⊢ \cdot_{𝑖} (X) = \cdot_{𝑖} (X)$
44	1 34 43	ssipeq	$⊢ U \in S \to \cdot_{𝑖} (X) = \cdot_{𝑖} (W)$
45	44	oveqd	$⊢ U \in S \to x \cdot_{𝑖} (X) y = x \cdot_{𝑖} (W) y$
46	45	eleq1d	$⊢ U \in S \to (x \cdot_{𝑖} (X) y \in {Base}_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)})$
47	46	adantl	$⊢ (W \in PreHil \land U \in S) \to (x \cdot_{𝑖} (X) y \in {Base}_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)})$
48	47	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to (x \cdot_{𝑖} (X) y \in {Base}_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (X)})$
49	42 48	mpbird	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to x \cdot_{𝑖} (X) y \in {Base}_{Scalar (X)}$
50	29	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to W \in PreHil$
51	7	adantr	$⊢ (W \in PreHil \land U \in S) \to W \in LMod$
52	51	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to W \in LMod$
53	25	fveq2d	$⊢ (W \in PreHil \land U \in S) \to {Base}_{Scalar (X)} = {Base}_{Scalar (W)}$
54	53	eleq2d	$⊢ (W \in PreHil \land U \in S) \to (q \in {Base}_{Scalar (X)} \leftrightarrow q \in {Base}_{Scalar (W)})$
55	54	biimpa	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)}) \to q \in {Base}_{Scalar (W)}$
56	55	3adant3	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to q \in {Base}_{Scalar (W)}$
57	32	3ad2ant1	$⊢ (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X}) \to x \in {Base}_{W}$
58	57	3ad2ant3	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to x \in {Base}_{W}$
59		eqid	$⊢ \cdot_{W} = \cdot_{W}$
60	30 22 59 35	lmodvscl	$⊢ (W \in LMod \land q \in {Base}_{Scalar (W)} \land x \in {Base}_{W}) \to q \cdot_{W} x \in {Base}_{W}$
61	52 56 58 60	syl3anc	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to q \cdot_{W} x \in {Base}_{W}$
62	33	3ad2ant2	$⊢ (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X}) \to y \in {Base}_{W}$
63	62	3ad2ant3	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to y \in {Base}_{W}$
64	31	sseli	$⊢ z \in {Base}_{X} \to z \in {Base}_{W}$
65	64	3ad2ant3	$⊢ (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X}) \to z \in {Base}_{W}$
66	65	3ad2ant3	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to z \in {Base}_{W}$
67		eqid	$⊢ +_{W} = +_{W}$
68		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
69	22 34 30 67 68	ipdir	$⊢ (W \in PreHil \land (q \cdot_{W} x \in {Base}_{W} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = ((q \cdot_{W} x) \cdot_{𝑖} (W) z) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
70	50 61 63 66 69	syl13anc	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = ((q \cdot_{W} x) \cdot_{𝑖} (W) z) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
71		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
72	22 34 30 35 59 71	ipass	$⊢ (W \in PreHil \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land z \in {Base}_{W})) \to (q \cdot_{W} x) \cdot_{𝑖} (W) z = q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)$
73	50 56 58 66 72	syl13anc	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to (q \cdot_{W} x) \cdot_{𝑖} (W) z = q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)$
74	73	oveq1d	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to ((q \cdot_{W} x) \cdot_{𝑖} (W) z) +_{Scalar (W)} (y \cdot_{𝑖} (W) z) = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
75	70 74	eqtrd	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
76	1 67	ressplusg	$⊢ U \in S \to +_{W} = +_{X}$
77	76	eqcomd	$⊢ U \in S \to +_{X} = +_{W}$
78	1 59	ressvsca	$⊢ U \in S \to \cdot_{W} = \cdot_{X}$
79	78	eqcomd	$⊢ U \in S \to \cdot_{X} = \cdot_{W}$
80	79	oveqd	$⊢ U \in S \to q \cdot_{X} x = q \cdot_{W} x$
81		eqidd	$⊢ U \in S \to y = y$
82	77 80 81	oveq123d	$⊢ U \in S \to (q \cdot_{X} x) +_{X} y = (q \cdot_{W} x) +_{W} y$
83		eqidd	$⊢ U \in S \to z = z$
84	44 82 83	oveq123d	$⊢ U \in S \to ((q \cdot_{X} x) +_{X} y) \cdot_{𝑖} (X) z = ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z$
85	24	fveq2d	$⊢ U \in S \to +_{Scalar (X)} = +_{Scalar (W)}$
86	24	fveq2d	$⊢ U \in S \to \cdot_{Scalar (X)} = \cdot_{Scalar (W)}$
87		eqidd	$⊢ U \in S \to q = q$
88	44	oveqd	$⊢ U \in S \to x \cdot_{𝑖} (X) z = x \cdot_{𝑖} (W) z$
89	86 87 88	oveq123d	$⊢ U \in S \to q \cdot_{Scalar (X)} (x \cdot_{𝑖} (X) z) = q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)$
90	44	oveqd	$⊢ U \in S \to y \cdot_{𝑖} (X) z = y \cdot_{𝑖} (W) z$
91	85 89 90	oveq123d	$⊢ U \in S \to (q \cdot_{Scalar (X)} (x \cdot_{𝑖} (X) z)) +_{Scalar (X)} (y \cdot_{𝑖} (X) z) = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
92	84 91	eqeq12d	$⊢ U \in S \to (((q \cdot_{X} x) +_{X} y) \cdot_{𝑖} (X) z = (q \cdot_{Scalar (X)} (x \cdot_{𝑖} (X) z)) +_{Scalar (X)} (y \cdot_{𝑖} (X) z) \leftrightarrow ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z))$
93	92	adantl	$⊢ (W \in PreHil \land U \in S) \to (((q \cdot_{X} x) +_{X} y) \cdot_{𝑖} (X) z = (q \cdot_{Scalar (X)} (x \cdot_{𝑖} (X) z)) +_{Scalar (X)} (y \cdot_{𝑖} (X) z) \leftrightarrow ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z))$
94	93	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to (((q \cdot_{X} x) +_{X} y) \cdot_{𝑖} (X) z = (q \cdot_{Scalar (X)} (x \cdot_{𝑖} (X) z)) +_{Scalar (X)} (y \cdot_{𝑖} (X) z) \leftrightarrow ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z))$
95	75 94	mpbird	$⊢ ((W \in PreHil \land U \in S) \land q \in {Base}_{Scalar (X)} \land (x \in {Base}_{X} \land y \in {Base}_{X} \land z \in {Base}_{X})) \to ((q \cdot_{X} x) +_{X} y) \cdot_{𝑖} (X) z = (q \cdot_{Scalar (X)} (x \cdot_{𝑖} (X) z)) +_{Scalar (X)} (y \cdot_{𝑖} (X) z)$
96	44	adantl	$⊢ (W \in PreHil \land U \in S) \to \cdot_{𝑖} (X) = \cdot_{𝑖} (W)$
97	96	oveqdr	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X}) \to x \cdot_{𝑖} (X) x = x \cdot_{𝑖} (W) x$
98	24	fveq2d	$⊢ U \in S \to 0_{Scalar (X)} = 0_{Scalar (W)}$
99	98	adantl	$⊢ (W \in PreHil \land U \in S) \to 0_{Scalar (X)} = 0_{Scalar (W)}$
100	99	adantr	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X}) \to 0_{Scalar (X)} = 0_{Scalar (W)}$
101	97 100	eqeq12d	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X}) \to (x \cdot_{𝑖} (X) x = 0_{Scalar (X)} \leftrightarrow x \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
102		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
103	22 34 30 102 8	ipeq0	$⊢ (W \in PreHil \land x \in {Base}_{W}) \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \leftrightarrow x = 0_{W})$
104	29 32 103	syl2an	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X}) \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \leftrightarrow x = 0_{W})$
105	104	biimpd	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X}) \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W})$
106	101 105	sylbid	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X}) \to (x \cdot_{𝑖} (X) x = 0_{Scalar (X)} \to x = 0_{W})$
107	106	3impia	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land x \cdot_{𝑖} (X) x = 0_{Scalar (X)}) \to x = 0_{W}$
108	24	fveq2d	$⊢ U \in S \to _{Scalar (X)} = _{Scalar (W)}$
109	108	fveq1d	$⊢ U \in S \to {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}} = {(x \cdot_{𝑖} (W) y)}^{_{Scalar (W)}}$
110	109	adantl	$⊢ (W \in PreHil \land U \in S) \to {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}} = {(x \cdot_{𝑖} (W) y)}^{_{Scalar (W)}}$
111	110	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}} = {(x \cdot_{𝑖} (W) y)}^{_{Scalar (W)}}$
112		eqid	$⊢ _{Scalar (W)} = _{Scalar (W)}$
113	22 34 30 112	ipcj	$⊢ (W \in PreHil \land x \in {Base}_{W} \land y \in {Base}_{W}) \to {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x$
114	29 32 33 113	syl3an	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x$
115	111 114	eqtrd	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (X)}} = y \cdot_{𝑖} (W) x$
116	45	fveq2d	$⊢ U \in S \to {(x \cdot_{𝑖} (X) y)}^{_{Scalar (X)}} = {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}}$
117	44	oveqd	$⊢ U \in S \to y \cdot_{𝑖} (X) x = y \cdot_{𝑖} (W) x$
118	116 117	eqeq12d	$⊢ U \in S \to ({(x \cdot_{𝑖} (X) y)}^{_{Scalar (X)}} = y \cdot_{𝑖} (X) x \leftrightarrow {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}} = y \cdot_{𝑖} (W) x)$
119	118	adantl	$⊢ (W \in PreHil \land U \in S) \to ({(x \cdot_{𝑖} (X) y)}^{_{Scalar (X)}} = y \cdot_{𝑖} (X) x \leftrightarrow {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}} = y \cdot_{𝑖} (W) x)$
120	119	3ad2ant1	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to ({(x \cdot_{𝑖} (X) y)}^{_{Scalar (X)}} = y \cdot_{𝑖} (X) x \leftrightarrow {(x \cdot_{𝑖} (W) y)}^{_{Scalar (X)}} = y \cdot_{𝑖} (W) x)$
121	115 120	mpbird	$⊢ ((W \in PreHil \land U \in S) \land x \in {Base}_{X} \land y \in {Base}_{X}) \to {(x \cdot_{𝑖} (X) y)}^{*_{Scalar (X)}} = y \cdot_{𝑖} (X) x$
122	3 4 5 6 12 13 14 15 16 17 18 21 28 49 95 107 121	isphld	$⊢ (W \in PreHil \land U \in S) \to X \in PreHil$

Metamath Proof Explorer

Theorem phlssphl

Proof