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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1plmhm.2 ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1plmhm.4 ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
r1plmhm.5 ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1plmhm.6 ⊢ 𝐹 = ( 𝑓 ∈ 𝑈 ↦ ( 𝑓 𝐸 𝑀 ) )
r1plmhm.9 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
r1plmhm.10 ⊢ ( 𝜑 → 𝑀 ∈ 𝑁 )
r1pquslmic.0 ⊢ 0 = ( 0g ‘ 𝑃 )
r1pquslmic.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
r1pquslmic.q ⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝐾 ) )
Assertion r1pquslmic ( 𝜑 → 𝑄 ≃𝑚 ( 𝐹 “s 𝑃 ) )

Proof

Step Hyp Ref Expression
1 r1plmhm.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1plmhm.2 ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1plmhm.4 ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
4 r1plmhm.5 ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
5 r1plmhm.6 ⊢ 𝐹 = ( 𝑓 ∈ 𝑈 ↦ ( 𝑓 𝐸 𝑀 ) )
6 r1plmhm.9 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 r1plmhm.10 ⊢ ( 𝜑 → 𝑀 ∈ 𝑁 )
8 r1pquslmic.0 ⊢ 0 = ( 0g ‘ 𝑃 )
9 r1pquslmic.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
10 r1pquslmic.q ⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝐾 ) )
11 eqidd ⊢ ( 𝜑 → ( 𝐹 “s 𝑃 ) = ( 𝐹 “s 𝑃 ) )
12 2 a1i ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑃 ) )
13 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → 𝑅 ∈ Ring )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → 𝑓 ∈ 𝑈 )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → 𝑀 ∈ 𝑁 )
17 3 1 2 4 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑀 ∈ 𝑁 ) → ( 𝑓 𝐸 𝑀 ) ∈ 𝑈 )
18 14 15 16 17 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → ( 𝑓 𝐸 𝑀 ) ∈ 𝑈 )
19 18 5 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ 𝑈 )
20 fimadmfo ⊢ ( 𝐹 : 𝑈 ⟶ 𝑈 → 𝐹 : 𝑈 –onto→ ( 𝐹 “ 𝑈 ) )
21 19 20 syl ⊢ ( 𝜑 → 𝐹 : 𝑈 –onto→ ( 𝐹 “ 𝑈 ) )
22 anass ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ↔ ( 𝜑 ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) )
23 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) )
24 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) )
25 23 24 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ ( 𝐹 “s 𝑃 ) ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝐹 “s 𝑃 ) ) ( 𝐹 ‘ 𝑞 ) ) )
26 1 2 3 4 5 6 7 r1plmhm ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 LMHom ( 𝐹 “s 𝑃 ) ) )
27 26 lmhmghmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 GrpHom ( 𝐹 “s 𝑃 ) ) )
28 27 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝐹 ∈ ( 𝑃 GrpHom ( 𝐹 “s 𝑃 ) ) )
29 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑎 ∈ 𝑈 )
30 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑏 ∈ 𝑈 )
31 eqid ⊢ ( +g ‘ ( 𝐹 “s 𝑃 ) ) = ( +g ‘ ( 𝐹 “s 𝑃 ) )
32 2 13 31 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑃 GrpHom ( 𝐹 “s 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ ( 𝐹 “s 𝑃 ) ) ( 𝐹 ‘ 𝑏 ) ) )
33 28 29 30 32 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ ( 𝐹 “s 𝑃 ) ) ( 𝐹 ‘ 𝑏 ) ) )
34 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑓 ∈ 𝑈 )
35 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑞 ∈ 𝑈 )
36 2 13 31 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑃 GrpHom ( 𝐹 “s 𝑃 ) ) ∧ 𝑓 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) → ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) = ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝐹 “s 𝑃 ) ) ( 𝐹 ‘ 𝑞 ) ) )
37 28 34 35 36 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) = ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝐹 “s 𝑃 ) ) ( 𝐹 ‘ 𝑞 ) ) )
38 25 33 37 3eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) )
39 38 expl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑓 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
40 39 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ ( 𝑓 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
41 22 40 sylanbr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) ∧ ( 𝑓 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
42 41 3impa ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ ( 𝑓 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑓 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑓 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
43 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
44 6 43 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
45 44 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
46 45 grpmndd ⊢ ( 𝜑 → 𝑃 ∈ Mnd )
47 11 12 13 21 42 46 8 imasmnd ⊢ ( 𝜑 → ( ( 𝐹 “s 𝑃 ) ∈ Mnd ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ ( 𝐹 “s 𝑃 ) ) ) )
48 47 simprd ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ ( 𝐹 “s 𝑃 ) ) )
49 oveq1 ⊢ ( 𝑓 = 0 → ( 𝑓 𝐸 𝑀 ) = ( 0 𝐸 𝑀 ) )
50 1 2 4 3 6 7 8 r1p0 ⊢ ( 𝜑 → ( 0 𝐸 𝑀 ) = 0 )
51 49 50 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑓 = 0 ) → ( 𝑓 𝐸 𝑀 ) = 0 )
52 2 8 ring0cl ⊢ ( 𝑃 ∈ Ring → 0 ∈ 𝑈 )
53 44 52 syl ⊢ ( 𝜑 → 0 ∈ 𝑈 )
54 5 51 53 53 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
55 48 54 eqtr3d ⊢ ( 𝜑 → ( 0g ‘ ( 𝐹 “s 𝑃 ) ) = 0 )
56 55 sneqd ⊢ ( 𝜑 → { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } = { 0 } )
57 56 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) = ( ◡ 𝐹 “ { 0 } ) )
58 57 9 eqtr4di ⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) = 𝐾 )
59 58 oveq2d ⊢ ( 𝜑 → ( 𝑃 ~QG ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) ) = ( 𝑃 ~QG 𝐾 ) )
60 59 oveq2d ⊢ ( 𝜑 → ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) ) ) = ( 𝑃 /s ( 𝑃 ~QG 𝐾 ) ) )
61 60 10 eqtr4di ⊢ ( 𝜑 → ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) ) ) = 𝑄 )
62 eqid ⊢ ( 0g ‘ ( 𝐹 “s 𝑃 ) ) = ( 0g ‘ ( 𝐹 “s 𝑃 ) )
63 eqid ⊢ ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) = ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } )
64 eqid ⊢ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) ) ) = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) ) )
65 19 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑈 )
66 fnima ⊢ ( 𝐹 Fn 𝑈 → ( 𝐹 “ 𝑈 ) = ran 𝐹 )
67 65 66 syl ⊢ ( 𝜑 → ( 𝐹 “ 𝑈 ) = ran 𝐹 )
68 1 fvexi ⊢ 𝑃 ∈ V
69 68 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
70 11 12 21 69 imasbas ⊢ ( 𝜑 → ( 𝐹 “ 𝑈 ) = ( Base ‘ ( 𝐹 “s 𝑃 ) ) )
71 67 70 eqtr3d ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ ( 𝐹 “s 𝑃 ) ) )
72 62 26 63 64 71 lmicqusker ⊢ ( 𝜑 → ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐹 “ { ( 0g ‘ ( 𝐹 “s 𝑃 ) ) } ) ) ) ≃𝑚 ( 𝐹 “s 𝑃 ) )
73 61 72 eqbrtrrd ⊢ ( 𝜑 → 𝑄 ≃𝑚 ( 𝐹 “s 𝑃 ) )