ipass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. (Contributed by NM, 25-Aug-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$⊢ F = Scalar (W)$
	phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	phllmhm.v	$⊢ V = {Base}_{W}$
	ipdir.f	$⊢ K = {Base}_{F}$
	ipass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	ipass.p	$⊢ \underset{˙}{\times} = \cdot_{F}$
Assertion	ipass	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (A \underset{˙}{\cdot} B) \underset{˙}{,} C = A \underset{˙}{\times} (B \underset{˙}{,} C)$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$⊢ F = Scalar (W)$
2		phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		phllmhm.v	$⊢ V = {Base}_{W}$
4		ipdir.f	$⊢ K = {Base}_{F}$
5		ipass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		ipass.p	$⊢ \underset{˙}{\times} = \cdot_{F}$
7		eqid	$⊢ (x \in V ⟼ x \underset{˙}{,} C) = (x \in V ⟼ x \underset{˙}{,} C)$
8	1 2 3 7	phllmhm	$⊢ (W \in PreHil \land C \in V) \to (x \in V ⟼ x \underset{˙}{,} C) \in (W LMHom ringLMod (F))$
9	8	3ad2antr3	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) \in (W LMHom ringLMod (F))$
10		simpr1	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to A \in K$
11		simpr2	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to B \in V$
12		rlmvsca	$⊢ \cdot_{F} = \cdot_{ringLMod (F)}$
13	6 12	eqtri	$⊢ \underset{˙}{\times} = \cdot_{ringLMod (F)}$
14	1 4 3 5 13	lmhmlin	$⊢ ((x \in V ⟼ x \underset{˙}{,} C) \in (W LMHom ringLMod (F)) \land A \in K \land B \in V) \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{\cdot} B) = A \underset{˙}{\times} (x \in V ⟼ x \underset{˙}{,} C) (B)$
15	9 10 11 14	syl3anc	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{\cdot} B) = A \underset{˙}{\times} (x \in V ⟼ x \underset{˙}{,} C) (B)$
16		phllmod	$⊢ W \in PreHil \to W \in LMod$
17	16	adantr	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to W \in LMod$
18	3 1 5 4	lmodvscl	$⊢ (W \in LMod \land A \in K \land B \in V) \to A \underset{˙}{\cdot} B \in V$
19	17 10 11 18	syl3anc	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to A \underset{˙}{\cdot} B \in V$
20		oveq1	$⊢ x = A \underset{˙}{\cdot} B \to x \underset{˙}{,} C = (A \underset{˙}{\cdot} B) \underset{˙}{,} C$
21		ovex	$⊢ x \underset{˙}{,} C \in V$
22	20 7 21	fvmpt3i	$⊢ A \underset{˙}{\cdot} B \in V \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{\cdot} B) = (A \underset{˙}{\cdot} B) \underset{˙}{,} C$
23	19 22	syl	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (A \underset{˙}{\cdot} B) = (A \underset{˙}{\cdot} B) \underset{˙}{,} C$
24		oveq1	$⊢ x = B \to x \underset{˙}{,} C = B \underset{˙}{,} C$
25	24 7 21	fvmpt3i	$⊢ B \in V \to (x \in V ⟼ x \underset{˙}{,} C) (B) = B \underset{˙}{,} C$
26	11 25	syl	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (x \in V ⟼ x \underset{˙}{,} C) (B) = B \underset{˙}{,} C$
27	26	oveq2d	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to A \underset{˙}{\times} (x \in V ⟼ x \underset{˙}{,} C) (B) = A \underset{˙}{\times} (B \underset{˙}{,} C)$
28	15 23 27	3eqtr3d	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (A \underset{˙}{\cdot} B) \underset{˙}{,} C = A \underset{˙}{\times} (B \underset{˙}{,} C)$

Metamath Proof Explorer

Theorem ipass

Proof