phssip

Description: The inner product (as a function) on a subspace is a restriction of the inner product (as a function) on the parent space. (Contributed by NM, 28-Jan-2008) (Revised by AV, 19-Oct-2021)

	Ref	Expression
Hypotheses	phssip.x	$⊢ X = W ↾_{𝑠} U$
	phssip.s	$⊢ S = LSubSp (W)$
	phssip.i	$⊢ \underset{˙}{\cdot} = \cdot_{if} (W)$
	phssip.p	$⊢ P = \cdot_{if} (X)$
Assertion	phssip	$⊢ (W \in PreHil \land U \in S) \to P = {\underset{˙}{\cdot} ↾}_{(U \times U)}$

Proof

Step	Hyp	Ref	Expression
1		phssip.x	$⊢ X = W ↾_{𝑠} U$
2		phssip.s	$⊢ S = LSubSp (W)$
3		phssip.i	$⊢ \underset{˙}{\cdot} = \cdot_{if} (W)$
4		phssip.p	$⊢ P = \cdot_{if} (X)$
5		eqid	$⊢ {Base}_{X} = {Base}_{X}$
6		eqid	$⊢ \cdot_{𝑖} (X) = \cdot_{𝑖} (X)$
7	5 6 4	ipffval	$⊢ P = (x \in {Base}_{X}, y \in {Base}_{X} ⟼ x \cdot_{𝑖} (X) y)$
8		phllmod	$⊢ W \in PreHil \to W \in LMod$
9	2	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
10	8 9	sylan	$⊢ (W \in PreHil \land U \in S) \to U \in SubGrp (W)$
11	1	subgbas	$⊢ U \in SubGrp (W) \to U = {Base}_{X}$
12	10 11	syl	$⊢ (W \in PreHil \land U \in S) \to U = {Base}_{X}$
13		eqidd	$⊢ (W \in PreHil \land U \in S) \to x \cdot_{𝑖} (W) y = x \cdot_{𝑖} (W) y$
14	12 12 13	mpoeq123dv	$⊢ (W \in PreHil \land U \in S) \to (x \in U, y \in U ⟼ x \cdot_{𝑖} (W) y) = (x \in {Base}_{X}, y \in {Base}_{X} ⟼ x \cdot_{𝑖} (W) y)$
15		eqid	$⊢ {Base}_{W} = {Base}_{W}$
16	15	subgss	$⊢ U \in SubGrp (W) \to U \subseteq {Base}_{W}$
17	10 16	syl	$⊢ (W \in PreHil \land U \in S) \to U \subseteq {Base}_{W}$
18		resmpo	$⊢ (U \subseteq {Base}_{W} \land U \subseteq {Base}_{W}) \to {(x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y) ↾}_{(U \times U)} = (x \in U, y \in U ⟼ x \cdot_{𝑖} (W) y)$
19	17 17 18	syl2anc	$⊢ (W \in PreHil \land U \in S) \to {(x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y) ↾}_{(U \times U)} = (x \in U, y \in U ⟼ x \cdot_{𝑖} (W) y)$
20		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
21	1 20 6	ssipeq	$⊢ U \in S \to \cdot_{𝑖} (X) = \cdot_{𝑖} (W)$
22	21	adantl	$⊢ (W \in PreHil \land U \in S) \to \cdot_{𝑖} (X) = \cdot_{𝑖} (W)$
23	22	oveqd	$⊢ (W \in PreHil \land U \in S) \to x \cdot_{𝑖} (X) y = x \cdot_{𝑖} (W) y$
24	23	mpoeq3dv	$⊢ (W \in PreHil \land U \in S) \to (x \in {Base}_{X}, y \in {Base}_{X} ⟼ x \cdot_{𝑖} (X) y) = (x \in {Base}_{X}, y \in {Base}_{X} ⟼ x \cdot_{𝑖} (W) y)$
25	14 19 24	3eqtr4rd	$⊢ (W \in PreHil \land U \in S) \to (x \in {Base}_{X}, y \in {Base}_{X} ⟼ x \cdot_{𝑖} (X) y) = {(x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y) ↾}_{(U \times U)}$
26	7 25	syl5eq	$⊢ (W \in PreHil \land U \in S) \to P = {(x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y) ↾}_{(U \times U)}$
27	15 20 3	ipffval	$⊢ \underset{˙}{\cdot} = (x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y)$
28	27	a1i	$⊢ (W \in PreHil \land U \in S) \to \underset{˙}{\cdot} = (x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y)$
29	28	reseq1d	$⊢ (W \in PreHil \land U \in S) \to {\underset{˙}{\cdot} ↾}_{(U \times U)} = {(x \in {Base}_{W}, y \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y) ↾}_{(U \times U)}$
30	26 29	eqtr4d	$⊢ (W \in PreHil \land U \in S) \to P = {\underset{˙}{\cdot} ↾}_{(U \times U)}$

Metamath Proof Explorer

Theorem phssip

Proof