clmvslinv

Description: Minus a vector plus itself. (Contributed by NM, 4-Dec-2006) (Revised by AV, 28-Sep-2021)

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

Step	Hyp	Ref	Expression
1		clmpm1dir.v	$⊢ V = {Base}_{W}$
2		clmpm1dir.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		clmpm1dir.a	$⊢ \underset{˙}{+} = +_{W}$
4		clmvsrinv.0	$⊢ \underset{˙}{0} = 0_{W}$
5		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7	1 5 6 2	clmvneg1	$⊢ (W \in CMod \land A \in V) \to -1 \underset{˙}{\cdot} A = {inv}_{g} (W) (A)$
8	7	oveq1d	$⊢ (W \in CMod \land A \in V) \to (-1 \underset{˙}{\cdot} A) \underset{˙}{+} A = {inv}_{g} (W) (A) \underset{˙}{+} A$
9		clmgrp	$⊢ W \in CMod \to W \in Grp$
10	1 3 4 5	grplinv	$⊢ (W \in Grp \land A \in V) \to {inv}_{g} (W) (A) \underset{˙}{+} A = \underset{˙}{0}$
11	9 10	sylan	$⊢ (W \in CMod \land A \in V) \to {inv}_{g} (W) (A) \underset{˙}{+} A = \underset{˙}{0}$
12	8 11	eqtrd	$⊢ (W \in CMod \land A \in V) \to (-1 \underset{˙}{\cdot} A) \underset{˙}{+} A = \underset{˙}{0}$

Metamath Proof Explorer