clmnegsubdi2

Description: Distribution of negative over vector subtraction. (Contributed by NM, 6-Aug-2007) (Revised by AV, 29-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		clmpm1dir.v	$⊢ V = {Base}_{W}$
2		clmpm1dir.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		clmpm1dir.a	$⊢ \underset{˙}{+} = +_{W}$
4		simp1	$⊢ (W \in CMod \land A \in V \land B \in V) \to W \in CMod$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
7	5 6	clmneg1	$⊢ W \in CMod \to - 1 \in {Base}_{Scalar (W)}$
8	7	3ad2ant1	$⊢ (W \in CMod \land A \in V \land B \in V) \to - 1 \in {Base}_{Scalar (W)}$
9		simp2	$⊢ (W \in CMod \land A \in V \land B \in V) \to A \in V$
10		simpl	$⊢ (W \in CMod \land B \in V) \to W \in CMod$
11	7	adantr	$⊢ (W \in CMod \land B \in V) \to - 1 \in {Base}_{Scalar (W)}$
12		simpr	$⊢ (W \in CMod \land B \in V) \to B \in V$
13	1 5 2 6	clmvscl	$⊢ (W \in CMod \land - 1 \in {Base}_{Scalar (W)} \land B \in V) \to -1 \underset{˙}{\cdot} B \in V$
14	10 11 12 13	syl3anc	$⊢ (W \in CMod \land B \in V) \to -1 \underset{˙}{\cdot} B \in V$
15	14	3adant2	$⊢ (W \in CMod \land A \in V \land B \in V) \to -1 \underset{˙}{\cdot} B \in V$
16	1 5 2 6 3	clmvsdi	$⊢ (W \in CMod \land (- 1 \in {Base}_{Scalar (W)} \land A \in V \land -1 \underset{˙}{\cdot} B \in V)) \to -1 \underset{˙}{\cdot} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = (-1 \underset{˙}{\cdot} A) \underset{˙}{+} (-1 \underset{˙}{\cdot} (-1 \underset{˙}{\cdot} B))$
17	4 8 9 15 16	syl13anc	$⊢ (W \in CMod \land A \in V \land B \in V) \to -1 \underset{˙}{\cdot} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = (-1 \underset{˙}{\cdot} A) \underset{˙}{+} (-1 \underset{˙}{\cdot} (-1 \underset{˙}{\cdot} B))$
18	1 2 3	clmnegneg	$⊢ (W \in CMod \land B \in V) \to -1 \underset{˙}{\cdot} (-1 \underset{˙}{\cdot} B) = B$
19	18	3adant2	$⊢ (W \in CMod \land A \in V \land B \in V) \to -1 \underset{˙}{\cdot} (-1 \underset{˙}{\cdot} B) = B$
20	19	oveq2d	$⊢ (W \in CMod \land A \in V \land B \in V) \to (-1 \underset{˙}{\cdot} A) \underset{˙}{+} (-1 \underset{˙}{\cdot} (-1 \underset{˙}{\cdot} B)) = (-1 \underset{˙}{\cdot} A) \underset{˙}{+} B$
21		clmabl	$⊢ W \in CMod \to W \in Abel$
22	21	3ad2ant1	$⊢ (W \in CMod \land A \in V \land B \in V) \to W \in Abel$
23		simpl	$⊢ (W \in CMod \land A \in V) \to W \in CMod$
24	7	adantr	$⊢ (W \in CMod \land A \in V) \to - 1 \in {Base}_{Scalar (W)}$
25		simpr	$⊢ (W \in CMod \land A \in V) \to A \in V$
26	1 5 2 6	clmvscl	$⊢ (W \in CMod \land - 1 \in {Base}_{Scalar (W)} \land A \in V) \to -1 \underset{˙}{\cdot} A \in V$
27	23 24 25 26	syl3anc	$⊢ (W \in CMod \land A \in V) \to -1 \underset{˙}{\cdot} A \in V$
28	27	3adant3	$⊢ (W \in CMod \land A \in V \land B \in V) \to -1 \underset{˙}{\cdot} A \in V$
29		simp3	$⊢ (W \in CMod \land A \in V \land B \in V) \to B \in V$
30	1 3	ablcom	$⊢ (W \in Abel \land -1 \underset{˙}{\cdot} A \in V \land B \in V) \to (-1 \underset{˙}{\cdot} A) \underset{˙}{+} B = B \underset{˙}{+} (-1 \underset{˙}{\cdot} A)$
31	22 28 29 30	syl3anc	$⊢ (W \in CMod \land A \in V \land B \in V) \to (-1 \underset{˙}{\cdot} A) \underset{˙}{+} B = B \underset{˙}{+} (-1 \underset{˙}{\cdot} A)$
32	17 20 31	3eqtrd	$⊢ (W \in CMod \land A \in V \land B \in V) \to -1 \underset{˙}{\cdot} (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = B \underset{˙}{+} (-1 \underset{˙}{\cdot} A)$

Metamath Proof Explorer

Theorem clmnegsubdi2

Proof