Theorem clmsubdir

Description: Scalar multiplication distributive law for subtraction. ( lmodsubdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clmsubdir.v	|- V = ( Base ` W )
	clmsubdir.t	|- .x. = ( .s ` W )
	clmsubdir.f	|- F = ( Scalar ` W )
	clmsubdir.k	|- K = ( Base ` F )
	clmsubdir.m	|- .- = ( -g ` W )
	clmsubdir.w	|- ( ph -> W e. CMod )
	clmsubdir.a	|- ( ph -> A e. K )
	clmsubdir.b	|- ( ph -> B e. K )
	clmsubdir.x	|- ( ph -> X e. V )
Assertion	clmsubdir	|- ( ph -> ( ( A - B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )

Proof

Step	Hyp	Ref	Expression
1		clmsubdir.v	|- V = ( Base ` W )
2		clmsubdir.t	|- .x. = ( .s ` W )
3		clmsubdir.f	|- F = ( Scalar ` W )
4		clmsubdir.k	|- K = ( Base ` F )
5		clmsubdir.m	|- .- = ( -g ` W )
6		clmsubdir.w	|- ( ph -> W e. CMod )
7		clmsubdir.a	|- ( ph -> A e. K )
8		clmsubdir.b	|- ( ph -> B e. K )
9		clmsubdir.x	|- ( ph -> X e. V )
10	3 4	clmsub	|- ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` F ) B ) )
11	6 7 8 10	syl3anc	|- ( ph -> ( A - B ) = ( A ( -g ` F ) B ) )
12	11	oveq1d	|- ( ph -> ( ( A - B ) .x. X ) = ( ( A ( -g ` F ) B ) .x. X ) )
13		eqid	|- ( -g ` F ) = ( -g ` F )
14		clmlmod	|- ( W e. CMod -> W e. LMod )
15	6 14	syl	|- ( ph -> W e. LMod )
16	1 2 3 4 5 13 15 7 8 9	lmodsubdir	|- ( ph -> ( ( A ( -g ` F ) B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )
17	12 16	eqtrd	|- ( ph -> ( ( A - B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )