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 )