Metamath Proof Explorer


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 = Base W
slmdvs1.f F = Scalar W
slmdvs1.s · ˙ = W
slmdvs1.u 1 ˙ = 1 F
Assertion slmdvs1 W SLMod X V 1 ˙ · ˙ X = X

Proof

Step Hyp Ref Expression
1 slmdvs1.v V = Base W
2 slmdvs1.f F = Scalar W
3 slmdvs1.s · ˙ = W
4 slmdvs1.u 1 ˙ = 1 F
5 simpl W SLMod X V W SLMod
6 eqid Base F = Base F
7 2 6 4 slmd1cl W SLMod 1 ˙ Base F
8 7 adantr W SLMod X V 1 ˙ Base F
9 simpr W SLMod X V X V
10 eqid + W = + W
11 eqid 0 W = 0 W
12 eqid + F = + F
13 eqid F = F
14 eqid 0 F = 0 F
15 1 10 3 11 2 6 12 13 4 14 slmdlema W SLMod 1 ˙ Base F 1 ˙ Base F X V X V 1 ˙ · ˙ X V 1 ˙ · ˙ X + W X = 1 ˙ · ˙ X + W 1 ˙ · ˙ X 1 ˙ + F 1 ˙ · ˙ X = 1 ˙ · ˙ X + W 1 ˙ · ˙ X 1 ˙ F 1 ˙ · ˙ X = 1 ˙ · ˙ 1 ˙ · ˙ X 1 ˙ · ˙ X = X 0 F · ˙ X = 0 W
16 15 simprd W SLMod 1 ˙ Base F 1 ˙ Base F X V X V 1 ˙ F 1 ˙ · ˙ X = 1 ˙ · ˙ 1 ˙ · ˙ X 1 ˙ · ˙ X = X 0 F · ˙ X = 0 W
17 16 simp2d W SLMod 1 ˙ Base F 1 ˙ Base F X V X V 1 ˙ · ˙ X = X
18 5 8 8 9 9 17 syl122anc W SLMod X V 1 ˙ · ˙ X = X