Theorem lmodvsdi

Description: Distributive law for scalar product (left-distributivity). ( ax-hvdistr1 analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	lmodvsdi.v	|- V = ( Base ` W )
	lmodvsdi.a	|- .+ = ( +g ` W )
	lmodvsdi.f	|- F = ( Scalar ` W )
	lmodvsdi.s	|- .x. = ( .s ` W )
	lmodvsdi.k	|- K = ( Base ` F )
Assertion	lmodvsdi	|- ( ( W e. LMod /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodvsdi.v	|- V = ( Base ` W )
2		lmodvsdi.a	|- .+ = ( +g ` W )
3		lmodvsdi.f	|- F = ( Scalar ` W )
4		lmodvsdi.s	|- .x. = ( .s ` W )
5		lmodvsdi.k	|- K = ( Base ` F )
6		eqid	|- ( +g ` F ) = ( +g ` F )
7		eqid	|- ( .r ` F ) = ( .r ` F )
8		eqid	|- ( 1r ` F ) = ( 1r ` F )
9	1 2 4 3 5 6 7 8	lmodlema	|- ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( Y e. V /\ X e. V ) ) -> ( ( ( R .x. X ) e. V /\ ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) .+ ( R .x. X ) ) ) /\ ( ( ( R ( .r ` F ) R ) .x. X ) = ( R .x. ( R .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X ) ) )
10	9	simpld	|- ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( Y e. V /\ X e. V ) ) -> ( ( R .x. X ) e. V /\ ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) .+ ( R .x. X ) ) ) )
11	10	simp2d	|- ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( Y e. V /\ X e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )
12	11	3expia	|- ( ( W e. LMod /\ ( R e. K /\ R e. K ) ) -> ( ( Y e. V /\ X e. V ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) )
13	12	anabsan2	|- ( ( W e. LMod /\ R e. K ) -> ( ( Y e. V /\ X e. V ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) )
14	13	exp4b	|- ( W e. LMod -> ( R e. K -> ( Y e. V -> ( X e. V -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) ) ) )
15	14	com34	|- ( W e. LMod -> ( R e. K -> ( X e. V -> ( Y e. V -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) ) ) )
16	15	3imp2	|- ( ( W e. LMod /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )