Theorem lmodvs1

Description: Scalar product with the ring unity. ( ax-hvmulid analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmodvs1.v	|- V = ( Base ` W )
	lmodvs1.f	|- F = ( Scalar ` W )
	lmodvs1.s	|- .x. = ( .s ` W )
	lmodvs1.u	|- .1. = ( 1r ` F )
Assertion	lmodvs1	|- ( ( W e. LMod /\ X e. V ) -> ( .1. .x. X ) = X )

Proof

Step	Hyp	Ref	Expression
1		lmodvs1.v	|- V = ( Base ` W )
2		lmodvs1.f	|- F = ( Scalar ` W )
3		lmodvs1.s	|- .x. = ( .s ` W )
4		lmodvs1.u	|- .1. = ( 1r ` F )
5		simpl	|- ( ( W e. LMod /\ X e. V ) -> W e. LMod )
6		eqid	|- ( Base ` F ) = ( Base ` F )
7	2 6 4	lmod1cl	|- ( W e. LMod -> .1. e. ( Base ` F ) )
8	7	adantr	|- ( ( W e. LMod /\ X e. V ) -> .1. e. ( Base ` F ) )
9		simpr	|- ( ( W e. LMod /\ X e. V ) -> X e. V )
10		eqid	|- ( +g ` W ) = ( +g ` W )
11		eqid	|- ( +g ` F ) = ( +g ` F )
12		eqid	|- ( .r ` F ) = ( .r ` F )
13	1 10 3 2 6 11 12 4	lmodlema	|- ( ( W e. LMod /\ ( .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 ) ) )
14	13	simprrd	|- ( ( W e. LMod /\ ( .1. e. ( Base ` F ) /\ .1. e. ( Base ` F ) ) /\ ( X e. V /\ X e. V ) ) -> ( .1. .x. X ) = X )
15	5 8 8 9 9 14	syl122anc	|- ( ( W e. LMod /\ X e. V ) -> ( .1. .x. X ) = X )