Theorem lmodvs1

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

	Ref	Expression
Hypotheses	lmodvs1.v	$$⊢V={\mathrm{Base}}_W$$
	lmodvs1.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmodvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmodvs1.u	$$⊢\underset{\dot{}}{1}=1_F$$
Assertion	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$

Proof

Step	Hyp	Ref	Expression
1		lmodvs1.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodvs1.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		lmodvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		lmodvs1.u	$$⊢\underset{\dot{}}{1}=1_F$$
5		simpl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to W\in \mathrm{LMod}$$
6		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
7	2 6 4	lmod1cl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_F$$
8	7	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_F$$
9		simpr	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\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	$$⊢\left(W\in \mathrm{LMod}\wedge \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_F\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_F\right)\wedge \left(X\in V\wedge X\in V\right)\right)\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\in V\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}\left(X{+}_{W}X\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right){+}_W\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\wedge \left(\underset{\dot{}}{1}{+}_F\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right){+}_W\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\right)\wedge \left(\left(\underset{\dot{}}{1}{\cdot }_F\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}X=X\right)\right)$$
14	13	simprrd	$$⊢\left(W\in \mathrm{LMod}\wedge \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_F\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_F\right)\wedge \left(X\in V\wedge X\in V\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$
15	5 8 8 9 9 14	syl122anc	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$