Metamath Proof Explorer

Theorem r1pquslmic

Description: The univariate polynomial remainder ring ( F "s P ) is module isomorphic with the quotient ring. (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 )
r1pquslmic.0 
|- .0. = ( 0g ` P )
r1pquslmic.k 
|- K = ( `' F " { .0. } )
r1pquslmic.q 
|- Q = ( P /s ( P ~QG K ) )
Assertion r1pquslmic 
|- ( ph -> Q ~=m ( 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 r1pquslmic.0 
 |-  .0. = ( 0g ` P )
9 r1pquslmic.k 
 |-  K = ( `' F " { .0. } )
10 r1pquslmic.q 
 |-  Q = ( P /s ( P ~QG K ) )
11 eqidd 
 |-  ( ph -> ( F "s P ) = ( F "s P ) )
12 2 a1i 
 |-  ( ph -> U = ( Base ` P ) )
13 eqid 
 |-  ( +g ` P ) = ( +g ` P )
14 6 adantr 
 |-  ( ( ph /\ f e. U ) -> R e. Ring )
15 simpr 
 |-  ( ( ph /\ f e. U ) -> f e. U )
16 7 adantr 
 |-  ( ( ph /\ f e. U ) -> M e. N )
17 3 1 2 4 r1pcl 
 |-  ( ( R e. Ring /\ f e. U /\ M e. N ) -> ( f E M ) e. U )
18 14 15 16 17 syl3anc 
 |-  ( ( ph /\ f e. U ) -> ( f E M ) e. U )
19 18 5 fmptd 
 |-  ( ph -> F : U --> U )
20 fimadmfo 
 |-  ( F : U --> U -> F : U -onto-> ( F " U ) )
21 19 20 syl 
 |-  ( ph -> F : U -onto-> ( F " U ) )
22 anass 
 |-  ( ( ( ph /\ a e. U ) /\ b e. U ) <-> ( ph /\ ( a e. U /\ b e. U ) ) )
23 simplr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` a ) = ( F ` f ) )
24 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` b ) = ( F ` q ) )
25 23 24 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( ( F ` a ) ( +g ` ( F "s P ) ) ( F ` b ) ) = ( ( F ` f ) ( +g ` ( F "s P ) ) ( F ` q ) ) )
26 1 2 3 4 5 6 7 r1plmhm 
 |-  ( ph -> F e. ( P LMHom ( F "s P ) ) )
27 26 lmhmghmd 
 |-  ( ph -> F e. ( P GrpHom ( F "s P ) ) )
28 27 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> F e. ( P GrpHom ( F "s P ) ) )
29 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> a e. U )
30 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> b e. U )
31 eqid 
 |-  ( +g ` ( F "s P ) ) = ( +g ` ( F "s P ) )
32 2 13 31 ghmlin 
 |-  ( ( F e. ( P GrpHom ( F "s P ) ) /\ a e. U /\ b e. U ) -> ( F ` ( a ( +g ` P ) b ) ) = ( ( F ` a ) ( +g ` ( F "s P ) ) ( F ` b ) ) )
33 28 29 30 32 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( ( F ` a ) ( +g ` ( F "s P ) ) ( F ` b ) ) )
34 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> f e. U )
35 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> q e. U )
36 2 13 31 ghmlin 
 |-  ( ( F e. ( P GrpHom ( F "s P ) ) /\ f e. U /\ q e. U ) -> ( F ` ( f ( +g ` P ) q ) ) = ( ( F ` f ) ( +g ` ( F "s P ) ) ( F ` q ) ) )
37 28 34 35 36 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( f ( +g ` P ) q ) ) = ( ( F ` f ) ( +g ` ( F "s P ) ) ( F ` q ) ) )
38 25 33 37 3eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) /\ ( F ` a ) = ( F ` f ) ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( f ( +g ` P ) q ) ) )
39 38 expl 
 |-  ( ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ f e. U ) /\ q e. U ) -> ( ( ( F ` a ) = ( F ` f ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( f ( +g ` P ) q ) ) ) )
40 39 anasss 
 |-  ( ( ( ( ph /\ a e. U ) /\ b e. U ) /\ ( f e. U /\ q e. U ) ) -> ( ( ( F ` a ) = ( F ` f ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( f ( +g ` P ) q ) ) ) )
41 22 40 sylanbr 
 |-  ( ( ( ph /\ ( a e. U /\ b e. U ) ) /\ ( f e. U /\ q e. U ) ) -> ( ( ( F ` a ) = ( F ` f ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( f ( +g ` P ) q ) ) ) )
42 41 3impa 
 |-  ( ( ph /\ ( a e. U /\ b e. U ) /\ ( f e. U /\ q e. U ) ) -> ( ( ( F ` a ) = ( F ` f ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` P ) b ) ) = ( F ` ( f ( +g ` P ) q ) ) ) )
43 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
44 6 43 syl 
 |-  ( ph -> P e. Ring )
45 44 ringgrpd 
 |-  ( ph -> P e. Grp )
46 45 grpmndd 
 |-  ( ph -> P e. Mnd )
47 11 12 13 21 42 46 8 imasmnd 
 |-  ( ph -> ( ( F "s P ) e. Mnd /\ ( F ` .0. ) = ( 0g ` ( F "s P ) ) ) )
48 47 simprd 
 |-  ( ph -> ( F ` .0. ) = ( 0g ` ( F "s P ) ) )
49 oveq1 
 |-  ( f = .0. -> ( f E M ) = ( .0. E M ) )
50 1 2 4 3 6 7 8 r1p0 
 |-  ( ph -> ( .0. E M ) = .0. )
51 49 50 sylan9eqr 
 |-  ( ( ph /\ f = .0. ) -> ( f E M ) = .0. )
52 2 8 ring0cl 
 |-  ( P e. Ring -> .0. e. U )
53 44 52 syl 
 |-  ( ph -> .0. e. U )
54 5 51 53 53 fvmptd2 
 |-  ( ph -> ( F ` .0. ) = .0. )
55 48 54 eqtr3d 
 |-  ( ph -> ( 0g ` ( F "s P ) ) = .0. )
56 55 sneqd 
 |-  ( ph -> { ( 0g ` ( F "s P ) ) } = { .0. } )
57 56 imaeq2d 
 |-  ( ph -> ( `' F " { ( 0g ` ( F "s P ) ) } ) = ( `' F " { .0. } ) )
58 57 9 eqtr4di 
 |-  ( ph -> ( `' F " { ( 0g ` ( F "s P ) ) } ) = K )
59 58 oveq2d 
 |-  ( ph -> ( P ~QG ( `' F " { ( 0g ` ( F "s P ) ) } ) ) = ( P ~QG K ) )
60 59 oveq2d 
 |-  ( ph -> ( P /s ( P ~QG ( `' F " { ( 0g ` ( F "s P ) ) } ) ) ) = ( P /s ( P ~QG K ) ) )
61 60 10 eqtr4di 
 |-  ( ph -> ( P /s ( P ~QG ( `' F " { ( 0g ` ( F "s P ) ) } ) ) ) = Q )
62 eqid 
 |-  ( 0g ` ( F "s P ) ) = ( 0g ` ( F "s P ) )
63 eqid 
 |-  ( `' F " { ( 0g ` ( F "s P ) ) } ) = ( `' F " { ( 0g ` ( F "s P ) ) } )
64 eqid 
 |-  ( P /s ( P ~QG ( `' F " { ( 0g ` ( F "s P ) ) } ) ) ) = ( P /s ( P ~QG ( `' F " { ( 0g ` ( F "s P ) ) } ) ) )
65 19 ffnd 
 |-  ( ph -> F Fn U )
66 fnima 
 |-  ( F Fn U -> ( F " U ) = ran F )
67 65 66 syl 
 |-  ( ph -> ( F " U ) = ran F )
68 1 fvexi 
 |-  P e. _V
69 68 a1i 
 |-  ( ph -> P e. _V )
70 11 12 21 69 imasbas 
 |-  ( ph -> ( F " U ) = ( Base ` ( F "s P ) ) )
71 67 70 eqtr3d 
 |-  ( ph -> ran F = ( Base ` ( F "s P ) ) )
72 62 26 63 64 71 lmicqusker 
 |-  ( ph -> ( P /s ( P ~QG ( `' F " { ( 0g ` ( F "s P ) ) } ) ) ) ~=m ( F "s P ) )
73 61 72 eqbrtrrd 
 |-  ( ph -> Q ~=m ( F "s P ) )