cphsubdir

Description: Distributive law for inner product subtraction. Complex version of ipsubdir . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cphipcj.v	$⊢ V = {Base}_{W}$
	cphsubdir.m	$⊢ \underset{˙}{-} = -_{W}$
Assertion	cphsubdir	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{-} B) \underset{˙}{,} C = (A \underset{˙}{,} C) - (B \underset{˙}{,} C)$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
2		cphipcj.v	$⊢ V = {Base}_{W}$
3		cphsubdir.m	$⊢ \underset{˙}{-} = -_{W}$
4		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		eqid	$⊢ -_{Scalar (W)} = -_{Scalar (W)}$
7	5 1 2 3 6	ipsubdir	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{-} B) \underset{˙}{,} C = (A \underset{˙}{,} C) -_{Scalar (W)} (B \underset{˙}{,} C)$
8	4 7	sylan	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{-} B) \underset{˙}{,} C = (A \underset{˙}{,} C) -_{Scalar (W)} (B \underset{˙}{,} C)$
9		cphclm	$⊢ W \in CPreHil \to W \in CMod$
10	9	adantr	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to W \in CMod$
11	4	adantr	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to W \in PreHil$
12		simpr1	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to A \in V$
13		simpr3	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to C \in V$
14		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
15	5 1 2 14	ipcl	$⊢ (W \in PreHil \land A \in V \land C \in V) \to A \underset{˙}{,} C \in {Base}_{Scalar (W)}$
16	11 12 13 15	syl3anc	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to A \underset{˙}{,} C \in {Base}_{Scalar (W)}$
17		simpr2	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to B \in V$
18	5 1 2 14	ipcl	$⊢ (W \in PreHil \land B \in V \land C \in V) \to B \underset{˙}{,} C \in {Base}_{Scalar (W)}$
19	11 17 13 18	syl3anc	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to B \underset{˙}{,} C \in {Base}_{Scalar (W)}$
20	5 14	clmsub	$⊢ (W \in CMod \land A \underset{˙}{,} C \in {Base}_{Scalar (W)} \land B \underset{˙}{,} C \in {Base}_{Scalar (W)}) \to (A \underset{˙}{,} C) - (B \underset{˙}{,} C) = (A \underset{˙}{,} C) -_{Scalar (W)} (B \underset{˙}{,} C)$
21	10 16 19 20	syl3anc	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{,} C) - (B \underset{˙}{,} C) = (A \underset{˙}{,} C) -_{Scalar (W)} (B \underset{˙}{,} C)$
22	8 21	eqtr4d	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land C \in V)) \to (A \underset{˙}{-} B) \underset{˙}{,} C = (A \underset{˙}{,} C) - (B \underset{˙}{,} C)$

Metamath Proof Explorer

Theorem cphsubdir

Proof