Metamath Proof Explorer

Theorem lmhmvsca

Description: The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses lmhmvsca.v 
|- V = ( Base ` M )
lmhmvsca.s 
|- .x. = ( .s ` N )
lmhmvsca.j 
|- J = ( Scalar ` N )
lmhmvsca.k 
|- K = ( Base ` J )
Assertion lmhmvsca 
|- ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( V X. { A } ) oF .x. F ) e. ( M LMHom N ) )

Proof

Step Hyp Ref Expression
1 lmhmvsca.v 
 |-  V = ( Base ` M )
2 lmhmvsca.s 
 |-  .x. = ( .s ` N )
3 lmhmvsca.j 
 |-  J = ( Scalar ` N )
4 lmhmvsca.k 
 |-  K = ( Base ` J )
5 eqid 
 |-  ( .s ` M ) = ( .s ` M )
6 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
7 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
8 lmhmlmod1 
 |-  ( F e. ( M LMHom N ) -> M e. LMod )
9 8 3ad2ant3 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> M e. LMod )
10 lmhmlmod2 
 |-  ( F e. ( M LMHom N ) -> N e. LMod )
11 10 3ad2ant3 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> N e. LMod )
12 6 3 lmhmsca 
 |-  ( F e. ( M LMHom N ) -> J = ( Scalar ` M ) )
13 12 3ad2ant3 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> J = ( Scalar ` M ) )
14 1 fvexi 
 |-  V e. _V
15 14 a1i 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> V e. _V )
16 simpl2 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ v e. V ) -> A e. K )
17 eqid 
 |-  ( Base ` N ) = ( Base ` N )
18 1 17 lmhmf 
 |-  ( F e. ( M LMHom N ) -> F : V --> ( Base ` N ) )
19 18 3ad2ant3 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> F : V --> ( Base ` N ) )
20 19 ffvelrnda 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ v e. V ) -> ( F ` v ) e. ( Base ` N ) )
21 fconstmpt 
 |-  ( V X. { A } ) = ( v e. V |-> A )
22 21 a1i 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( V X. { A } ) = ( v e. V |-> A ) )
23 19 feqmptd 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> F = ( v e. V |-> ( F ` v ) ) )
24 15 16 20 22 23 offval2 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( V X. { A } ) oF .x. F ) = ( v e. V |-> ( A .x. ( F ` v ) ) ) )
25 eqidd 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( u e. ( Base ` N ) |-> ( A .x. u ) ) = ( u e. ( Base ` N ) |-> ( A .x. u ) ) )
26 oveq2 
 |-  ( u = ( F ` v ) -> ( A .x. u ) = ( A .x. ( F ` v ) ) )
27 20 23 25 26 fmptco 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( u e. ( Base ` N ) |-> ( A .x. u ) ) o. F ) = ( v e. V |-> ( A .x. ( F ` v ) ) ) )
28 24 27 eqtr4d 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( V X. { A } ) oF .x. F ) = ( ( u e. ( Base ` N ) |-> ( A .x. u ) ) o. F ) )
29 simp2 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> A e. K )
30 17 3 2 4 lmodvsghm 
 |-  ( ( N e. LMod /\ A e. K ) -> ( u e. ( Base ` N ) |-> ( A .x. u ) ) e. ( N GrpHom N ) )
31 11 29 30 syl2anc 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( u e. ( Base ` N ) |-> ( A .x. u ) ) e. ( N GrpHom N ) )
32 lmghm 
 |-  ( F e. ( M LMHom N ) -> F e. ( M GrpHom N ) )
33 32 3ad2ant3 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> F e. ( M GrpHom N ) )
34 ghmco 
 |-  ( ( ( u e. ( Base ` N ) |-> ( A .x. u ) ) e. ( N GrpHom N ) /\ F e. ( M GrpHom N ) ) -> ( ( u e. ( Base ` N ) |-> ( A .x. u ) ) o. F ) e. ( M GrpHom N ) )
35 31 33 34 syl2anc 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( u e. ( Base ` N ) |-> ( A .x. u ) ) o. F ) e. ( M GrpHom N ) )
36 28 35 eqeltrd 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( V X. { A } ) oF .x. F ) e. ( M GrpHom N ) )
37 simpl1 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> J e. CRing )
38 simpl2 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> A e. K )
39 simprl 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> x e. ( Base ` ( Scalar ` M ) ) )
40 13 fveq2d 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( Base ` J ) = ( Base ` ( Scalar ` M ) ) )
41 4 40 syl5eq 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> K = ( Base ` ( Scalar ` M ) ) )
42 41 adantr 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> K = ( Base ` ( Scalar ` M ) ) )
43 39 42 eleqtrrd 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> x e. K )
44 eqid 
 |-  ( .r ` J ) = ( .r ` J )
45 4 44 crngcom 
 |-  ( ( J e. CRing /\ A e. K /\ x e. K ) -> ( A ( .r ` J ) x ) = ( x ( .r ` J ) A ) )
46 37 38 43 45 syl3anc 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( A ( .r ` J ) x ) = ( x ( .r ` J ) A ) )
47 46 oveq1d 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( ( A ( .r ` J ) x ) .x. ( F ` y ) ) = ( ( x ( .r ` J ) A ) .x. ( F ` y ) ) )
48 11 adantr 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> N e. LMod )
49 19 adantr 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> F : V --> ( Base ` N ) )
50 simprr 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> y e. V )
51 49 50 ffvelrnd 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( F ` y ) e. ( Base ` N ) )
52 17 3 2 4 44 lmodvsass 
 |-  ( ( N e. LMod /\ ( A e. K /\ x e. K /\ ( F ` y ) e. ( Base ` N ) ) ) -> ( ( A ( .r ` J ) x ) .x. ( F ` y ) ) = ( A .x. ( x .x. ( F ` y ) ) ) )
53 48 38 43 51 52 syl13anc 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( ( A ( .r ` J ) x ) .x. ( F ` y ) ) = ( A .x. ( x .x. ( F ` y ) ) ) )
54 17 3 2 4 44 lmodvsass 
 |-  ( ( N e. LMod /\ ( x e. K /\ A e. K /\ ( F ` y ) e. ( Base ` N ) ) ) -> ( ( x ( .r ` J ) A ) .x. ( F ` y ) ) = ( x .x. ( A .x. ( F ` y ) ) ) )
55 48 43 38 51 54 syl13anc 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( ( x ( .r ` J ) A ) .x. ( F ` y ) ) = ( x .x. ( A .x. ( F ` y ) ) ) )
56 47 53 55 3eqtr3d 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( A .x. ( x .x. ( F ` y ) ) ) = ( x .x. ( A .x. ( F ` y ) ) ) )
57 1 6 5 7 lmodvscl 
 |-  ( ( M e. LMod /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) -> ( x ( .s ` M ) y ) e. V )
58 57 3expb 
 |-  ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( x ( .s ` M ) y ) e. V )
59 9 58 sylan 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( x ( .s ` M ) y ) e. V )
60 14 a1i 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> V e. _V )
61 19 ffnd 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> F Fn V )
62 61 adantr 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> F Fn V )
63 6 7 1 5 2 lmhmlin 
 |-  ( ( F e. ( M LMHom N ) /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) -> ( F ` ( x ( .s ` M ) y ) ) = ( x .x. ( F ` y ) ) )
64 63 3expb 
 |-  ( ( F e. ( M LMHom N ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( F ` ( x ( .s ` M ) y ) ) = ( x .x. ( F ` y ) ) )
65 64 3ad2antl3 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( F ` ( x ( .s ` M ) y ) ) = ( x .x. ( F ` y ) ) )
66 65 adantr 
 |-  ( ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) /\ ( x ( .s ` M ) y ) e. V ) -> ( F ` ( x ( .s ` M ) y ) ) = ( x .x. ( F ` y ) ) )
67 60 38 62 66 ofc1 
 |-  ( ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) /\ ( x ( .s ` M ) y ) e. V ) -> ( ( ( V X. { A } ) oF .x. F ) ` ( x ( .s ` M ) y ) ) = ( A .x. ( x .x. ( F ` y ) ) ) )
68 59 67 mpdan 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( ( ( V X. { A } ) oF .x. F ) ` ( x ( .s ` M ) y ) ) = ( A .x. ( x .x. ( F ` y ) ) ) )
69 eqidd 
 |-  ( ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) /\ y e. V ) -> ( F ` y ) = ( F ` y ) )
70 60 38 62 69 ofc1 
 |-  ( ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) /\ y e. V ) -> ( ( ( V X. { A } ) oF .x. F ) ` y ) = ( A .x. ( F ` y ) ) )
71 50 70 mpdan 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( ( ( V X. { A } ) oF .x. F ) ` y ) = ( A .x. ( F ` y ) ) )
72 71 oveq2d 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( x .x. ( ( ( V X. { A } ) oF .x. F ) ` y ) ) = ( x .x. ( A .x. ( F ` y ) ) ) )
73 56 68 72 3eqtr4d 
 |-  ( ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. V ) ) -> ( ( ( V X. { A } ) oF .x. F ) ` ( x ( .s ` M ) y ) ) = ( x .x. ( ( ( V X. { A } ) oF .x. F ) ` y ) ) )
74 1 5 2 6 3 7 9 11 13 36 73 islmhmd 
 |-  ( ( J e. CRing /\ A e. K /\ F e. ( M LMHom N ) ) -> ( ( V X. { A } ) oF .x. F ) e. ( M LMHom N ) )