ipassr

Description: "Associative" law for second argument of inner product (compare ipass ). (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}$
	ipassr.i	$⊢ \underset{˙}{} = _{F}$
Assertion	ipassr	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to A \underset{˙}{,} (C \underset{˙}{\cdot} B) = (A \underset{˙}{,} B) \underset{˙}{\times} \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		ipassr.i	$⊢ \underset{˙}{} = _{F}$
8		simpl	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to W \in PreHil$
9		simpr3	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to C \in K$
10		simpr2	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to B \in V$
11		simpr1	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to A \in V$
12	1 2 3 4 5 6	ipass	$⊢ (W \in PreHil \land (C \in K \land B \in V \land A \in V)) \to (C \underset{˙}{\cdot} B) \underset{˙}{,} A = C \underset{˙}{\times} (B \underset{˙}{,} A)$
13	8 9 10 11 12	syl13anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to (C \underset{˙}{\cdot} B) \underset{˙}{,} A = C \underset{˙}{\times} (B \underset{˙}{,} A)$
14	13	fveq2d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to \underset{˙}{} ((C \underset{˙}{\cdot} B) \underset{˙}{,} A) = \underset{˙}{} (C \underset{˙}{\times} (B \underset{˙}{,} A))$
15		phllmod	$⊢ W \in PreHil \to W \in LMod$
16	15	adantr	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to W \in LMod$
17	3 1 5 4	lmodvscl	$⊢ (W \in LMod \land C \in K \land B \in V) \to C \underset{˙}{\cdot} B \in V$
18	16 9 10 17	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to C \underset{˙}{\cdot} B \in V$
19	1 2 3 7	ipcj	$⊢ (W \in PreHil \land C \underset{˙}{\cdot} B \in V \land A \in V) \to \underset{˙}{*} ((C \underset{˙}{\cdot} B) \underset{˙}{,} A) = A \underset{˙}{,} (C \underset{˙}{\cdot} B)$
20	8 18 11 19	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to \underset{˙}{*} ((C \underset{˙}{\cdot} B) \underset{˙}{,} A) = A \underset{˙}{,} (C \underset{˙}{\cdot} B)$
21	1	phlsrng	$⊢ W \in PreHil \to F \in *-Ring$
22	21	adantr	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to F \in *-Ring$
23	1 2 3 4	ipcl	$⊢ (W \in PreHil \land B \in V \land A \in V) \to B \underset{˙}{,} A \in K$
24	8 10 11 23	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to B \underset{˙}{,} A \in K$
25	7 4 6	srngmul	$⊢ (F \in -Ring \land C \in K \land B \underset{˙}{,} A \in K) \to \underset{˙}{} (C \underset{˙}{\times} (B \underset{˙}{,} A)) = \underset{˙}{} (B \underset{˙}{,} A) \underset{˙}{\times} \underset{˙}{} (C)$
26	22 9 24 25	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to \underset{˙}{} (C \underset{˙}{\times} (B \underset{˙}{,} A)) = \underset{˙}{} (B \underset{˙}{,} A) \underset{˙}{\times} \underset{˙}{*} (C)$
27	14 20 26	3eqtr3d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to A \underset{˙}{,} (C \underset{˙}{\cdot} B) = \underset{˙}{} (B \underset{˙}{,} A) \underset{˙}{\times} \underset{˙}{} (C)$
28	1 2 3 7	ipcj	$⊢ (W \in PreHil \land B \in V \land A \in V) \to \underset{˙}{*} (B \underset{˙}{,} A) = A \underset{˙}{,} B$
29	8 10 11 28	syl3anc	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to \underset{˙}{*} (B \underset{˙}{,} A) = A \underset{˙}{,} B$
30	29	oveq1d	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to \underset{˙}{} (B \underset{˙}{,} A) \underset{˙}{\times} \underset{˙}{} (C) = (A \underset{˙}{,} B) \underset{˙}{\times} \underset{˙}{*} (C)$
31	27 30	eqtrd	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in K)) \to A \underset{˙}{,} (C \underset{˙}{\cdot} B) = (A \underset{˙}{,} B) \underset{˙}{\times} \underset{˙}{*} (C)$

Metamath Proof Explorer

Theorem ipassr

Proof