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

Metamath Proof Explorer

Theorem lmodvs1

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

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

Proof

Step	Hyp	Ref	Expression
1		lmodvs1.v	$⊢ V = {Base}_{W}$
2		lmodvs1.f	$⊢ F = Scalar (W)$
3		lmodvs1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvs1.u	$⊢ \underset{˙}{1} = 1_{F}$
5		simpl	$⊢ (W \in LMod \land X \in V) \to W \in LMod$
6		eqid	$⊢ {Base}_{F} = {Base}_{F}$
7	2 6 4	lmod1cl	$⊢ W \in LMod \to \underset{˙}{1} \in {Base}_{F}$
8	7	adantr	$⊢ (W \in LMod \land X \in V) \to \underset{˙}{1} \in {Base}_{F}$
9		simpr	$⊢ (W \in LMod \land X \in V) \to X \in V$
10		eqid	$⊢ +_{W} = +_{W}$
11		eqid	$⊢ +_{F} = +_{F}$
12		eqid	$⊢ \cdot_{F} = \cdot_{F}$
13	1 10 3 2 6 11 12 4	lmodlema	$⊢ (W \in LMod \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))$
14	13	simprrd	$⊢ (W \in LMod \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$
15	5 8 8 9 9 14	syl122anc	$⊢ (W \in LMod \land X \in V) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$