cphassr

Description: "Associative" law for second argument of inner product (compare cphass ). See ipassr , his52 . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cphipcj.v	$⊢ V = {Base}_{W}$
	cphass.f	$⊢ F = Scalar (W)$
	cphass.k	$⊢ K = {Base}_{F}$
	cphass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	cphassr	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to B \underset{˙}{,} (A \underset{˙}{\cdot} C) = \overline{A} (B \underset{˙}{,} C)$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
2		cphipcj.v	$⊢ V = {Base}_{W}$
3		cphass.f	$⊢ F = Scalar (W)$
4		cphass.k	$⊢ K = {Base}_{F}$
5		cphass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		cphclm	$⊢ W \in CPreHil \to W \in CMod$
7	6	adantr	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to W \in CMod$
8	3	clmmul	$⊢ W \in CMod \to \times = \cdot_{F}$
9	7 8	syl	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to \times = \cdot_{F}$
10		eqidd	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to B \underset{˙}{,} C = B \underset{˙}{,} C$
11	3	clmcj	$⊢ W \in CMod \to * = *_{F}$
12	7 11	syl	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to * = *_{F}$
13	12	fveq1d	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to \overline{A} = A^{*_{F}}$
14	9 10 13	oveq123d	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to (B \underset{˙}{,} C) \overline{A} = (B \underset{˙}{,} C) \cdot_{F} A^{*_{F}}$
15	3 4	clmsscn	$⊢ W \in CMod \to K \subseteq ℂ$
16	7 15	syl	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to K \subseteq ℂ$
17		simpr1	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to A \in K$
18	16 17	sseldd	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to A \in ℂ$
19	18	cjcld	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to \overline{A} \in ℂ$
20	2 1	cphipcl	$⊢ (W \in CPreHil \land B \in V \land C \in V) \to B \underset{˙}{,} C \in ℂ$
21	20	3adant3r1	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to B \underset{˙}{,} C \in ℂ$
22	19 21	mulcomd	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to \overline{A} (B \underset{˙}{,} C) = (B \underset{˙}{,} C) \overline{A}$
23		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
24		3anrot	$⊢ (A \in K \land B \in V \land C \in V) \leftrightarrow (B \in V \land C \in V \land A \in K)$
25	24	biimpi	$⊢ (A \in K \land B \in V \land C \in V) \to (B \in V \land C \in V \land A \in K)$
26		eqid	$⊢ \cdot_{F} = \cdot_{F}$
27		eqid	$⊢ _{F} = _{F}$
28	3 1 2 4 5 26 27	ipassr	$⊢ (W \in PreHil \land (B \in V \land C \in V \land A \in K)) \to B \underset{˙}{,} (A \underset{˙}{\cdot} C) = (B \underset{˙}{,} C) \cdot_{F} A^{*_{F}}$
29	23 25 28	syl2an	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to B \underset{˙}{,} (A \underset{˙}{\cdot} C) = (B \underset{˙}{,} C) \cdot_{F} A^{*_{F}}$
30	14 22 29	3eqtr4rd	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to B \underset{˙}{,} (A \underset{˙}{\cdot} C) = \overline{A} (B \underset{˙}{,} C)$

Metamath Proof Explorer

Theorem cphassr

Proof