clmpm1dir

Description: Subtractive distributive law for the scalar product of a subcomplex module. (Contributed by NM, 31-Jul-2007) (Revised by AV, 21-Sep-2021)

	Ref	Expression
Hypotheses	clmpm1dir.v	$⊢ V = {Base}_{W}$
	clmpm1dir.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	clmpm1dir.a	$⊢ \underset{˙}{+} = +_{W}$
	clmpm1dir.k	$⊢ K = {Base}_{Scalar (W)}$
Assertion	clmpm1dir	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to (A - B) \underset{˙}{\cdot} C = (A \underset{˙}{\cdot} C) \underset{˙}{+} (-1 \underset{˙}{\cdot} (B \underset{˙}{\cdot} C))$

Proof

Step	Hyp	Ref	Expression
1		clmpm1dir.v	$⊢ V = {Base}_{W}$
2		clmpm1dir.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		clmpm1dir.a	$⊢ \underset{˙}{+} = +_{W}$
4		clmpm1dir.k	$⊢ K = {Base}_{Scalar (W)}$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		eqid	$⊢ -_{W} = -_{W}$
7		simpl	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to W \in CMod$
8		simpr1	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to A \in K$
9		simpr2	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to B \in K$
10		simpr3	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to C \in V$
11	1 2 5 4 6 7 8 9 10	clmsubdir	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to (A - B) \underset{˙}{\cdot} C = (A \underset{˙}{\cdot} C) -_{W} (B \underset{˙}{\cdot} C)$
12	1 5 2 4	clmvscl	$⊢ (W \in CMod \land A \in K \land C \in V) \to A \underset{˙}{\cdot} C \in V$
13	7 8 10 12	syl3anc	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to A \underset{˙}{\cdot} C \in V$
14	1 5 2 4	clmvscl	$⊢ (W \in CMod \land B \in K \land C \in V) \to B \underset{˙}{\cdot} C \in V$
15	7 9 10 14	syl3anc	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to B \underset{˙}{\cdot} C \in V$
16		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
17	1 3 16 6	grpsubval	$⊢ (A \underset{˙}{\cdot} C \in V \land B \underset{˙}{\cdot} C \in V) \to (A \underset{˙}{\cdot} C) -_{W} (B \underset{˙}{\cdot} C) = (A \underset{˙}{\cdot} C) \underset{˙}{+} {inv}_{g} (W) (B \underset{˙}{\cdot} C)$
18	13 15 17	syl2anc	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to (A \underset{˙}{\cdot} C) -_{W} (B \underset{˙}{\cdot} C) = (A \underset{˙}{\cdot} C) \underset{˙}{+} {inv}_{g} (W) (B \underset{˙}{\cdot} C)$
19	1 16 5 2	clmvneg1	$⊢ (W \in CMod \land B \underset{˙}{\cdot} C \in V) \to -1 \underset{˙}{\cdot} (B \underset{˙}{\cdot} C) = {inv}_{g} (W) (B \underset{˙}{\cdot} C)$
20	19	eqcomd	$⊢ (W \in CMod \land B \underset{˙}{\cdot} C \in V) \to {inv}_{g} (W) (B \underset{˙}{\cdot} C) = -1 \underset{˙}{\cdot} (B \underset{˙}{\cdot} C)$
21	7 15 20	syl2anc	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to {inv}_{g} (W) (B \underset{˙}{\cdot} C) = -1 \underset{˙}{\cdot} (B \underset{˙}{\cdot} C)$
22	21	oveq2d	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to (A \underset{˙}{\cdot} C) \underset{˙}{+} {inv}_{g} (W) (B \underset{˙}{\cdot} C) = (A \underset{˙}{\cdot} C) \underset{˙}{+} (-1 \underset{˙}{\cdot} (B \underset{˙}{\cdot} C))$
23	11 18 22	3eqtrd	$⊢ (W \in CMod \land (A \in K \land B \in K \land C \in V)) \to (A - B) \underset{˙}{\cdot} C = (A \underset{˙}{\cdot} C) \underset{˙}{+} (-1 \underset{˙}{\cdot} (B \underset{˙}{\cdot} C))$

Metamath Proof Explorer

Theorem clmpm1dir

Proof