cph2ass

Description: Move scalar multiplication to outside of inner product. See his35 . (Contributed by Mario Carneiro, 17-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	cph2ass	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to (A \underset{˙}{\cdot} C) \underset{˙}{,} (B \underset{˙}{\cdot} D) = A \overline{B} (C \underset{˙}{,} D)$

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		simp1	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to W \in CPreHil$
7		simp2r	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to B \in K$
8		simp3l	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to C \in V$
9		simp3r	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to D \in V$
10	1 2 3 4 5	cphassr	$⊢ (W \in CPreHil \land (B \in K \land C \in V \land D \in V)) \to C \underset{˙}{,} (B \underset{˙}{\cdot} D) = \overline{B} (C \underset{˙}{,} D)$
11	6 7 8 9 10	syl13anc	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to C \underset{˙}{,} (B \underset{˙}{\cdot} D) = \overline{B} (C \underset{˙}{,} D)$
12	11	oveq2d	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to A (C \underset{˙}{,} (B \underset{˙}{\cdot} D)) = A \overline{B} (C \underset{˙}{,} D)$
13		simp2l	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to A \in K$
14		cphlmod	$⊢ W \in CPreHil \to W \in LMod$
15	14	3ad2ant1	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to W \in LMod$
16	2 3 5 4	lmodvscl	$⊢ (W \in LMod \land B \in K \land D \in V) \to B \underset{˙}{\cdot} D \in V$
17	15 7 9 16	syl3anc	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to B \underset{˙}{\cdot} D \in V$
18	1 2 3 4 5	cphass	$⊢ (W \in CPreHil \land (A \in K \land C \in V \land B \underset{˙}{\cdot} D \in V)) \to (A \underset{˙}{\cdot} C) \underset{˙}{,} (B \underset{˙}{\cdot} D) = A (C \underset{˙}{,} (B \underset{˙}{\cdot} D))$
19	6 13 8 17 18	syl13anc	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to (A \underset{˙}{\cdot} C) \underset{˙}{,} (B \underset{˙}{\cdot} D) = A (C \underset{˙}{,} (B \underset{˙}{\cdot} D))$
20		cphclm	$⊢ W \in CPreHil \to W \in CMod$
21	20	3ad2ant1	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to W \in CMod$
22	3 4	clmsscn	$⊢ W \in CMod \to K \subseteq ℂ$
23	21 22	syl	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to K \subseteq ℂ$
24	23 13	sseldd	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to A \in ℂ$
25	23 7	sseldd	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to B \in ℂ$
26	25	cjcld	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to \overline{B} \in ℂ$
27	2 1	cphipcl	$⊢ (W \in CPreHil \land C \in V \land D \in V) \to C \underset{˙}{,} D \in ℂ$
28	27	3expb	$⊢ (W \in CPreHil \land (C \in V \land D \in V)) \to C \underset{˙}{,} D \in ℂ$
29	28	3adant2	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to C \underset{˙}{,} D \in ℂ$
30	24 26 29	mulassd	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to A \overline{B} (C \underset{˙}{,} D) = A \overline{B} (C \underset{˙}{,} D)$
31	12 19 30	3eqtr4d	$⊢ (W \in CPreHil \land (A \in K \land B \in K) \land (C \in V \land D \in V)) \to (A \underset{˙}{\cdot} C) \underset{˙}{,} (B \underset{˙}{\cdot} D) = A \overline{B} (C \underset{˙}{,} D)$

Metamath Proof Explorer

Theorem cph2ass

Proof