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

Metamath Proof Explorer

Theorem clmvs1

Description: Scalar product with ring unity. ( lmodvs1 analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmvs1.v 
|- V = ( Base ` W )
clmvs1.s 
|- .x. = ( .s ` W )
Assertion clmvs1 
|- ( ( W e. CMod /\ X e. V ) -> ( 1 .x. X ) = X )

Proof

Step Hyp Ref Expression
1 clmvs1.v 
 |-  V = ( Base ` W )
2 clmvs1.s 
 |-  .x. = ( .s ` W )
3 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
4 3 clm1 
 |-  ( W e. CMod -> 1 = ( 1r ` ( Scalar ` W ) ) )
5 4 adantr 
 |-  ( ( W e. CMod /\ X e. V ) -> 1 = ( 1r ` ( Scalar ` W ) ) )
6 5 oveq1d 
 |-  ( ( W e. CMod /\ X e. V ) -> ( 1 .x. X ) = ( ( 1r ` ( Scalar ` W ) ) .x. X ) )
7 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
8 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
9 1 3 2 8 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` ( Scalar ` W ) ) .x. X ) = X )
10 7 9 sylan 
 |-  ( ( W e. CMod /\ X e. V ) -> ( ( 1r ` ( Scalar ` W ) ) .x. X ) = X )
11 6 10 eqtrd 
 |-  ( ( W e. CMod /\ X e. V ) -> ( 1 .x. X ) = X )