Theorem slmdvs1

Description: Scalar product with ring unit. ( 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={\mathrm{Base}}_W$$
	slmdvs1.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	slmdvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	slmdvs1.u	$$⊢\underset{\dot{}}{1}=1_F$$
Assertion	slmdvs1	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$

Proof

Step	Hyp	Ref	Expression
1		slmdvs1.v	$$⊢V={\mathrm{Base}}_W$$
2		slmdvs1.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		slmdvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		slmdvs1.u	$$⊢\underset{\dot{}}{1}=1_F$$
5		simpl	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to W\in \mathrm{SLMod}$$
6		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
7	2 6 4	slmd1cl	$$⊢W\in \mathrm{SLMod}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_F$$
8	7	adantr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_F$$
9		simpr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\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	$$⊢\left(W\in \mathrm{SLMod}\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\wedge 0_F\underset{\dot{}}{·}X=0_W\right)\right)$$
16	15	simprd	$$⊢\left(W\in \mathrm{SLMod}\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}{\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\wedge 0_F\underset{\dot{}}{·}X=0_W\right)$$
17	16	simp2d	$$⊢\left(W\in \mathrm{SLMod}\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$$
18	5 8 8 9 9 17	syl122anc	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$