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 
|- .x. = ( .s ` W )
slmdvs1.u 
|- .1. = ( 1r ` F )
Assertion slmdvs1 
|- ( ( W e. SLMod /\ X e. V ) -> ( .1. .x. X ) = X )

Proof

Step Hyp Ref Expression
1 slmdvs1.v 
 |-  V = ( Base ` W )
2 slmdvs1.f 
 |-  F = ( Scalar ` W )
3 slmdvs1.s 
 |-  .x. = ( .s ` W )
4 slmdvs1.u 
 |-  .1. = ( 1r ` F )
5 simpl 
 |-  ( ( W e. SLMod /\ X e. V ) -> W e. SLMod )
6 eqid 
 |-  ( Base ` F ) = ( Base ` F )
7 2 6 4 slmd1cl 
 |-  ( W e. SLMod -> .1. e. ( Base ` F ) )
8 7 adantr 
 |-  ( ( W e. SLMod /\ X e. V ) -> .1. e. ( Base ` F ) )
9 simpr 
 |-  ( ( W e. SLMod /\ X e. V ) -> X e. V )
10 eqid 
 |-  ( +g ` W ) = ( +g ` W )
11 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
12 eqid 
 |-  ( +g ` F ) = ( +g ` F )
13 eqid 
 |-  ( .r ` F ) = ( .r ` F )
14 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
15 1 10 3 11 2 6 12 13 4 14 slmdlema 
 |-  ( ( W e. SLMod /\ ( .1. e. ( Base ` F ) /\ .1. e. ( Base ` F ) ) /\ ( X e. V /\ X e. V ) ) -> ( ( ( .1. .x. X ) e. V /\ ( .1. .x. ( X ( +g ` W ) X ) ) = ( ( .1. .x. X ) ( +g ` W ) ( .1. .x. X ) ) /\ ( ( .1. ( +g ` F ) .1. ) .x. X ) = ( ( .1. .x. X ) ( +g ` W ) ( .1. .x. X ) ) ) /\ ( ( ( .1. ( .r ` F ) .1. ) .x. X ) = ( .1. .x. ( .1. .x. X ) ) /\ ( .1. .x. X ) = X /\ ( ( 0g ` F ) .x. X ) = ( 0g ` W ) ) ) )
16 15 simprd 
 |-  ( ( W e. SLMod /\ ( .1. e. ( Base ` F ) /\ .1. e. ( Base ` F ) ) /\ ( X e. V /\ X e. V ) ) -> ( ( ( .1. ( .r ` F ) .1. ) .x. X ) = ( .1. .x. ( .1. .x. X ) ) /\ ( .1. .x. X ) = X /\ ( ( 0g ` F ) .x. X ) = ( 0g ` W ) ) )
17 16 simp2d 
 |-  ( ( W e. SLMod /\ ( .1. e. ( Base ` F ) /\ .1. e. ( Base ` F ) ) /\ ( X e. V /\ X e. V ) ) -> ( .1. .x. X ) = X )
18 5 8 8 9 9 17 syl122anc 
 |-  ( ( W e. SLMod /\ X e. V ) -> ( .1. .x. X ) = X )