Metamath Proof Explorer

Theorem r1plmhm

Description: The univariate polynomial remainder function F is a module homomorphism. Its image ( F "s P ) is sometimes called the "ring of remainders" (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses r1plmhm.1 
|- P = ( Poly1 ` R )
r1plmhm.2 
|- U = ( Base ` P )
r1plmhm.4 
|- E = ( rem1p ` R )
r1plmhm.5 
|- N = ( Unic1p ` R )
r1plmhm.6 
|- F = ( f e. U |-> ( f E M ) )
r1plmhm.9 
|- ( ph -> R e. Ring )
r1plmhm.10 
|- ( ph -> M e. N )
Assertion r1plmhm 
|- ( ph -> F e. ( P LMHom ( F "s P ) ) )

Proof

Step Hyp Ref Expression
1 r1plmhm.1 
 |-  P = ( Poly1 ` R )
2 r1plmhm.2 
 |-  U = ( Base ` P )
3 r1plmhm.4 
 |-  E = ( rem1p ` R )
4 r1plmhm.5 
 |-  N = ( Unic1p ` R )
5 r1plmhm.6 
 |-  F = ( f e. U |-> ( f E M ) )
6 r1plmhm.9 
 |-  ( ph -> R e. Ring )
7 r1plmhm.10 
 |-  ( ph -> M e. N )
8 6 adantr 
 |-  ( ( ph /\ f e. U ) -> R e. Ring )
9 simpr 
 |-  ( ( ph /\ f e. U ) -> f e. U )
10 7 adantr 
 |-  ( ( ph /\ f e. U ) -> M e. N )
11 3 1 2 4 r1pcl 
 |-  ( ( R e. Ring /\ f e. U /\ M e. N ) -> ( f E M ) e. U )
12 8 9 10 11 syl3anc 
 |-  ( ( ph /\ f e. U ) -> ( f E M ) e. U )
13 12 5 fmptd 
 |-  ( ph -> F : U --> U )
14 eqid 
 |-  ( +g ` P ) = ( +g ` P )
15 anass 
 |-  ( ( ( ph /\ a e. U ) /\ b e. U ) <-> ( ph /\ ( a e. U /\ b e. U ) ) )
16 6 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> R e. Ring )
17 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> a e. U )
18 7 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> M e. N )
19 simplr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` a ) = ( F ` p ) )
20 oveq1 
 |-  ( f = a -> ( f E M ) = ( a E M ) )
21 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( a E M ) e. _V )
22 5 20 17 21 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` a ) = ( a E M ) )
23 oveq1 
 |-  ( f = p -> ( f E M ) = ( p E M ) )
24 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> p e. U )
25 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( p E M ) e. _V )
26 5 23 24 25 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` p ) = ( p E M ) )
27 19 22 26 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( a E M ) = ( p E M ) )
28 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> b e. U )
29 1 2 4 3 16 17 18 27 14 24 28 r1padd1 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( a ( +g ` P ) b ) E M ) = ( ( p ( +g ` P ) b ) E M ) )
30 oveq1 
 |-  ( f = ( a ( +g ` P ) b ) -> ( f E M ) = ( ( a ( +g ` P ) b ) E M ) )
31 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
32 6 31 syl 
 |-  ( ph -> P e. Ring )
33 32 ringgrpd 
 |-  ( ph -> P e. Grp )
34 33 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> P e. Grp )
35 2 14 34 17 28 grpcld 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( a ( +g ` P ) b ) e. U )
36 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( a ( +g ` P ) b ) E M ) e. _V )
37 5 30 35 36 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( ( a ( +g ` P ) b ) E M ) )
38 oveq1 
 |-  ( f = ( p ( +g ` P ) b ) -> ( f E M ) = ( ( p ( +g ` P ) b ) E M ) )
39 2 14 34 24 28 grpcld 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( p ( +g ` P ) b ) e. U )
40 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( p ( +g ` P ) b ) E M ) e. _V )
41 5 38 39 40 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( p ( +g ` P ) b ) ) = ( ( p ( +g ` P ) b ) E M ) )
42 29 37 41 3eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( p ( +g ` P ) b ) ) )
43 32 ringabld 
 |-  ( ph -> P e. Abel )
44 43 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> P e. Abel )
45 2 14 ablcom 
 |-  ( ( P e. Abel /\ p e. U /\ b e. U ) -> ( p ( +g ` P ) b ) = ( b ( +g ` P ) p ) )
46 44 24 28 45 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( p ( +g ` P ) b ) = ( b ( +g ` P ) p ) )
47 46 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( p ( +g ` P ) b ) ) = ( F ` ( b ( +g ` P ) p ) ) )
48 42 47 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( b ( +g ` P ) p ) ) )
49 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` b ) = ( F ` q ) )
50 oveq1 
 |-  ( f = b -> ( f E M ) = ( b E M ) )
51 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( b E M ) e. _V )
52 5 50 28 51 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` b ) = ( b E M ) )
53 oveq1 
 |-  ( f = q -> ( f E M ) = ( q E M ) )
54 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> q e. U )
55 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( q E M ) e. _V )
56 5 53 54 55 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` q ) = ( q E M ) )
57 49 52 56 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( b E M ) = ( q E M ) )
58 1 2 4 3 16 28 18 57 14 54 24 r1padd1 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( b ( +g ` P ) p ) E M ) = ( ( q ( +g ` P ) p ) E M ) )
59 oveq1 
 |-  ( f = ( b ( +g ` P ) p ) -> ( f E M ) = ( ( b ( +g ` P ) p ) E M ) )
60 2 14 34 28 24 grpcld 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( b ( +g ` P ) p ) e. U )
61 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( b ( +g ` P ) p ) E M ) e. _V )
62 5 59 60 61 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( b ( +g ` P ) p ) ) = ( ( b ( +g ` P ) p ) E M ) )
63 oveq1 
 |-  ( f = ( q ( +g ` P ) p ) -> ( f E M ) = ( ( q ( +g ` P ) p ) E M ) )
64 2 14 34 54 24 grpcld 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( q ( +g ` P ) p ) e. U )
65 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( q ( +g ` P ) p ) E M ) e. _V )
66 5 63 64 65 fvmptd3 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( q ( +g ` P ) p ) ) = ( ( q ( +g ` P ) p ) E M ) )
67 58 62 66 3eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( b ( +g ` P ) p ) ) = ( F ` ( q ( +g ` P ) p ) ) )
68 2 14 ablcom 
 |-  ( ( P e. Abel /\ q e. U /\ p e. U ) -> ( q ( +g ` P ) p ) = ( p ( +g ` P ) q ) )
69 44 54 24 68 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( q ( +g ` P ) p ) = ( p ( +g ` P ) q ) )
70 69 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( q ( +g ` P ) p ) ) = ( F ` ( p ( +g ` P ) q ) ) )
71 48 67 70 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` p ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( p ( +g ` P ) q ) ) )
72 71 expl 
 |-  ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ p e. U ) /\ q e. U ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( p ( +g ` P ) q ) ) ) )
73 72 anasss 
 |-  ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ ( p e. U /\ q e. U ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( p ( +g ` P ) q ) ) ) )
74 15 73 sylanbr 
 |-  ( ( ( ph /\ ( a e. U /\ b e. U ) ) /\ ( p e. U /\ q e. U ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( p ( +g ` P ) q ) ) ) )
75 74 3impa 
 |-  ( ( ph /\ ( a e. U /\ b e. U ) /\ ( p e. U /\ q e. U ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( p ( +g ` P ) q ) ) ) )
76 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
77 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
78 simplr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( F ` a ) = ( F ` b ) )
79 simpr2 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> a e. U )
80 ovexd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( a E M ) e. _V )
81 5 20 79 80 fvmptd3 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( F ` a ) = ( a E M ) )
82 simpr3 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> b e. U )
83 ovexd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( b E M ) e. _V )
84 5 50 82 83 fvmptd3 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( F ` b ) = ( b E M ) )
85 78 81 84 3eqtr3d 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( a E M ) = ( b E M ) )
86 85 oveq2d 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( k ( .s ` P ) ( a E M ) ) = ( k ( .s ` P ) ( b E M ) ) )
87 6 ad2antrr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> R e. Ring )
88 7 ad2antrr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> M e. N )
89 eqid 
 |-  ( .s ` P ) = ( .s ` P )
90 eqid 
 |-  ( Base ` R ) = ( Base ` R )
91 simpr1 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> k e. ( Base ` ( Scalar ` P ) ) )
92 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
93 6 92 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
94 93 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
95 94 ad2antrr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
96 91 95 eleqtrrd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> k e. ( Base ` R ) )
97 1 2 4 3 87 79 88 89 90 96 r1pvsca 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( ( k ( .s ` P ) a ) E M ) = ( k ( .s ` P ) ( a E M ) ) )
98 1 2 4 3 87 82 88 89 90 96 r1pvsca 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( ( k ( .s ` P ) b ) E M ) = ( k ( .s ` P ) ( b E M ) ) )
99 86 97 98 3eqtr4d 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( ( k ( .s ` P ) a ) E M ) = ( ( k ( .s ` P ) b ) E M ) )
100 oveq1 
 |-  ( f = ( k ( .s ` P ) a ) -> ( f E M ) = ( ( k ( .s ` P ) a ) E M ) )
101 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
102 87 101 syl 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> P e. LMod )
103 2 76 89 77 102 91 79 lmodvscld 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( k ( .s ` P ) a ) e. U )
104 ovexd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( ( k ( .s ` P ) a ) E M ) e. _V )
105 5 100 103 104 fvmptd3 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( F ` ( k ( .s ` P ) a ) ) = ( ( k ( .s ` P ) a ) E M ) )
106 oveq1 
 |-  ( f = ( k ( .s ` P ) b ) -> ( f E M ) = ( ( k ( .s ` P ) b ) E M ) )
107 2 76 89 77 102 91 82 lmodvscld 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( k ( .s ` P ) b ) e. U )
108 ovexd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( ( k ( .s ` P ) b ) E M ) e. _V )
109 5 106 107 108 fvmptd3 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( F ` ( k ( .s ` P ) b ) ) = ( ( k ( .s ` P ) b ) E M ) )
110 99 105 109 3eqtr4d 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( F ` ( k ( .s ` P ) a ) ) = ( F ` ( k ( .s ` P ) b ) ) )
111 110 an32s 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) /\ ( F ` a ) = ( F ` b ) ) -> ( F ` ( k ( .s ` P ) a ) ) = ( F ` ( k ( .s ` P ) b ) ) )
112 111 ex 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ a e. U /\ b e. U ) ) -> ( ( F ` a ) = ( F ` b ) -> ( F ` ( k ( .s ` P ) a ) ) = ( F ` ( k ( .s ` P ) b ) ) ) )
113 6 101 syl 
 |-  ( ph -> P e. LMod )
114 2 13 14 75 76 77 112 113 89 imaslmhm 
 |-  ( ph -> ( ( F "s P ) e. LMod /\ F e. ( P LMHom ( F "s P ) ) ) )
115 114 simprd 
 |-  ( ph -> F e. ( P LMHom ( F "s P ) ) )