This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem slmdvs1

Description: Scalar product with ring unity. ( ax-hvmulid analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

		Ref	Expression
	Hypotheses	slmdvs1.v	$⊢ V = {Base}_{W}$
		slmdvs1.f	$⊢ F = Scalar (W)$
		slmdvs1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
		slmdvs1.u	$⊢ \underset{˙}{1} = 1_{F}$
	Assertion	slmdvs1	$⊢ (W \in SLMod \land X \in V) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$

Proof

Step	Hyp	Ref	Expression
1		slmdvs1.v	$⊢ V = {Base}_{W}$
2		slmdvs1.f	$⊢ F = Scalar (W)$
3		slmdvs1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		slmdvs1.u	$⊢ \underset{˙}{1} = 1_{F}$
5		simpl	$⊢ (W \in SLMod \land X \in V) \to W \in SLMod$
6		eqid	$⊢ {Base}_{F} = {Base}_{F}$
7	2 6 4	slmd1cl	$⊢ W \in SLMod \to \underset{˙}{1} \in {Base}_{F}$
8	7	adantr	$⊢ (W \in SLMod \land X \in V) \to \underset{˙}{1} \in {Base}_{F}$
9		simpr	$⊢ (W \in SLMod \land X \in V) \to X \in V$
10		eqid	$⊢ +_{W} = +_{W}$
11		eqid	$⊢ 0_{W} = 0_{W}$
12		eqid	$⊢ +_{F} = +_{F}$
13		eqid	$⊢ \cdot_{F} = \cdot_{F}$
14		eqid	$⊢ 0_{F} = 0_{F}$
15	1 10 3 11 2 6 12 13 4 14	slmdlema	$⊢ (W \in SLMod \land (\underset{˙}{1} \in {Base}_{F} \land \underset{˙}{1} \in {Base}_{F}) \land (X \in V \land X \in V)) \to ((\underset{˙}{1} \underset{˙}{\cdot} X \in V \land \underset{˙}{1} \underset{˙}{\cdot} (X +_{W} X) = (\underset{˙}{1} \underset{˙}{\cdot} X) +_{W} (\underset{˙}{1} \underset{˙}{\cdot} X) \land (\underset{˙}{1} +_{F} \underset{˙}{1}) \underset{˙}{\cdot} X = (\underset{˙}{1} \underset{˙}{\cdot} X) +_{W} (\underset{˙}{1} \underset{˙}{\cdot} X)) \land ((\underset{˙}{1} \cdot_{F} \underset{˙}{1}) \underset{˙}{\cdot} X = \underset{˙}{1} \underset{˙}{\cdot} (\underset{˙}{1} \underset{˙}{\cdot} X) \land \underset{˙}{1} \underset{˙}{\cdot} X = X \land 0_{F} \underset{˙}{\cdot} X = 0_{W}))$
16	15	simprd	$⊢ (W \in SLMod \land (\underset{˙}{1} \in {Base}_{F} \land \underset{˙}{1} \in {Base}_{F}) \land (X \in V \land X \in V)) \to ((\underset{˙}{1} \cdot_{F} \underset{˙}{1}) \underset{˙}{\cdot} X = \underset{˙}{1} \underset{˙}{\cdot} (\underset{˙}{1} \underset{˙}{\cdot} X) \land \underset{˙}{1} \underset{˙}{\cdot} X = X \land 0_{F} \underset{˙}{\cdot} X = 0_{W})$
17	16	simp2d	$⊢ (W \in SLMod \land (\underset{˙}{1} \in {Base}_{F} \land \underset{˙}{1} \in {Base}_{F}) \land (X \in V \land X \in V)) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$
18	5 8 8 9 9 17	syl122anc	$⊢ (W \in SLMod \land X \in V) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$