| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | evls1maprhm.u | . 2
⊢ 𝑈 = (Base‘𝑃) | 
| 2 |  | eqid 2736 | . 2
⊢
(1r‘𝑃) = (1r‘𝑃) | 
| 3 |  | eqid 2736 | . 2
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 4 |  | eqid 2736 | . 2
⊢
(.r‘𝑃) = (.r‘𝑃) | 
| 5 |  | eqid 2736 | . 2
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 6 |  | evls1maprhm.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 7 |  | evls1maprhm.s | . . . . 5
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) | 
| 8 |  | eqid 2736 | . . . . . 6
⊢ (𝑅 ↾s 𝑆) = (𝑅 ↾s 𝑆) | 
| 9 | 8 | subrgcrng 20576 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ (SubRing‘𝑅)) → (𝑅 ↾s 𝑆) ∈ CRing) | 
| 10 | 6, 7, 9 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ CRing) | 
| 11 |  | evls1maprhm.p | . . . . 5
⊢ 𝑃 =
(Poly1‘(𝑅
↾s 𝑆)) | 
| 12 | 11 | ply1crng 22201 | . . . 4
⊢ ((𝑅 ↾s 𝑆) ∈ CRing → 𝑃 ∈ CRing) | 
| 13 | 10, 12 | syl 17 | . . 3
⊢ (𝜑 → 𝑃 ∈ CRing) | 
| 14 | 13 | crngringd 20244 | . 2
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 15 | 6 | crngringd 20244 | . 2
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 16 |  | evls1maprhm.f | . . . 4
⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋)) | 
| 17 |  | fveq2 6905 | . . . . 5
⊢ (𝑝 = (1r‘𝑃) → (𝑂‘𝑝) = (𝑂‘(1r‘𝑃))) | 
| 18 | 17 | fveq1d 6907 | . . . 4
⊢ (𝑝 = (1r‘𝑃) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(1r‘𝑃))‘𝑋)) | 
| 19 | 1, 2 | ringidcl 20263 | . . . . 5
⊢ (𝑃 ∈ Ring →
(1r‘𝑃)
∈ 𝑈) | 
| 20 | 14, 19 | syl 17 | . . . 4
⊢ (𝜑 → (1r‘𝑃) ∈ 𝑈) | 
| 21 |  | fvexd 6920 | . . . 4
⊢ (𝜑 → ((𝑂‘(1r‘𝑃))‘𝑋) ∈ V) | 
| 22 | 16, 18, 20, 21 | fvmptd3 7038 | . . 3
⊢ (𝜑 → (𝐹‘(1r‘𝑃)) = ((𝑂‘(1r‘𝑃))‘𝑋)) | 
| 23 | 8, 3 | subrg1 20583 | . . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘(𝑅
↾s 𝑆))) | 
| 24 | 7, 23 | syl 17 | . . . . . . 7
⊢ (𝜑 → (1r‘𝑅) = (1r‘(𝑅 ↾s 𝑆))) | 
| 25 | 24 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → ((algSc‘𝑃)‘(1r‘𝑅)) = ((algSc‘𝑃)‘(1r‘(𝑅 ↾s 𝑆)))) | 
| 26 | 10 | crngringd 20244 | . . . . . . 7
⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Ring) | 
| 27 |  | eqid 2736 | . . . . . . . 8
⊢
(algSc‘𝑃) =
(algSc‘𝑃) | 
| 28 |  | eqid 2736 | . . . . . . . 8
⊢
(1r‘(𝑅 ↾s 𝑆)) = (1r‘(𝑅 ↾s 𝑆)) | 
| 29 | 11, 27, 28, 2 | ply1scl1 22297 | . . . . . . 7
⊢ ((𝑅 ↾s 𝑆) ∈ Ring →
((algSc‘𝑃)‘(1r‘(𝑅 ↾s 𝑆))) = (1r‘𝑃)) | 
| 30 | 26, 29 | syl 17 | . . . . . 6
⊢ (𝜑 → ((algSc‘𝑃)‘(1r‘(𝑅 ↾s 𝑆))) = (1r‘𝑃)) | 
| 31 | 25, 30 | eqtr2d 2777 | . . . . 5
⊢ (𝜑 → (1r‘𝑃) = ((algSc‘𝑃)‘(1r‘𝑅))) | 
| 32 | 31 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (𝑂‘(1r‘𝑃)) = (𝑂‘((algSc‘𝑃)‘(1r‘𝑅)))) | 
| 33 | 32 | fveq1d 6907 | . . 3
⊢ (𝜑 → ((𝑂‘(1r‘𝑃))‘𝑋) = ((𝑂‘((algSc‘𝑃)‘(1r‘𝑅)))‘𝑋)) | 
| 34 |  | evls1maprhm.q | . . . 4
⊢ 𝑂 = (𝑅 evalSub1 𝑆) | 
| 35 |  | evls1maprhm.b | . . . 4
⊢ 𝐵 = (Base‘𝑅) | 
| 36 | 3 | subrg1cl 20581 | . . . . 5
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(1r‘𝑅)
∈ 𝑆) | 
| 37 | 7, 36 | syl 17 | . . . 4
⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆) | 
| 38 |  | evls1maprhm.y | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 39 | 34, 11, 8, 35, 27, 6, 7, 37, 38 | evls1scafv 22371 | . . 3
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘(1r‘𝑅)))‘𝑋) = (1r‘𝑅)) | 
| 40 | 22, 33, 39 | 3eqtrd 2780 | . 2
⊢ (𝜑 → (𝐹‘(1r‘𝑃)) = (1r‘𝑅)) | 
| 41 | 6 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑅 ∈ CRing) | 
| 42 | 7 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑆 ∈ (SubRing‘𝑅)) | 
| 43 |  | simprl 770 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑞 ∈ 𝑈) | 
| 44 |  | simprr 772 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑟 ∈ 𝑈) | 
| 45 | 38 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑋 ∈ 𝐵) | 
| 46 | 34, 35, 11, 8, 1, 4,
5, 41, 42, 43, 44, 45 | evls1muld 22377 | . . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋) = (((𝑂‘𝑞)‘𝑋)(.r‘𝑅)((𝑂‘𝑟)‘𝑋))) | 
| 47 |  | fveq2 6905 | . . . . 5
⊢ (𝑝 = (𝑞(.r‘𝑃)𝑟) → (𝑂‘𝑝) = (𝑂‘(𝑞(.r‘𝑃)𝑟))) | 
| 48 | 47 | fveq1d 6907 | . . . 4
⊢ (𝑝 = (𝑞(.r‘𝑃)𝑟) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋)) | 
| 49 | 14 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑃 ∈ Ring) | 
| 50 | 1, 4, 49, 43, 44 | ringcld 20258 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝑞(.r‘𝑃)𝑟) ∈ 𝑈) | 
| 51 |  | fvexd 6920 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋) ∈ V) | 
| 52 | 16, 48, 50, 51 | fvmptd3 7038 | . . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(.r‘𝑃)𝑟)) = ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋)) | 
| 53 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑞 → (𝑂‘𝑝) = (𝑂‘𝑞)) | 
| 54 | 53 | fveq1d 6907 | . . . . 5
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘𝑞)‘𝑋)) | 
| 55 |  | fvexd 6920 | . . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘𝑞)‘𝑋) ∈ V) | 
| 56 | 16, 54, 43, 55 | fvmptd3 7038 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘𝑞) = ((𝑂‘𝑞)‘𝑋)) | 
| 57 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑟 → (𝑂‘𝑝) = (𝑂‘𝑟)) | 
| 58 | 57 | fveq1d 6907 | . . . . 5
⊢ (𝑝 = 𝑟 → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘𝑟)‘𝑋)) | 
| 59 |  | fvexd 6920 | . . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘𝑟)‘𝑋) ∈ V) | 
| 60 | 16, 58, 44, 59 | fvmptd3 7038 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘𝑟) = ((𝑂‘𝑟)‘𝑋)) | 
| 61 | 56, 60 | oveq12d 7450 | . . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝐹‘𝑞)(.r‘𝑅)(𝐹‘𝑟)) = (((𝑂‘𝑞)‘𝑋)(.r‘𝑅)((𝑂‘𝑟)‘𝑋))) | 
| 62 | 46, 52, 61 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(.r‘𝑃)𝑟)) = ((𝐹‘𝑞)(.r‘𝑅)(𝐹‘𝑟))) | 
| 63 |  | eqid 2736 | . 2
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 64 |  | eqid 2736 | . 2
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 65 |  | eqid 2736 | . . . . . . . . 9
⊢
(eval1‘𝑅) = (eval1‘𝑅) | 
| 66 | 34, 35, 11, 8, 1, 65, 6, 7 | ressply1evl 22375 | . . . . . . . 8
⊢ (𝜑 → 𝑂 = ((eval1‘𝑅) ↾ 𝑈)) | 
| 67 | 66 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑂 = ((eval1‘𝑅) ↾ 𝑈)) | 
| 68 | 67 | fveq1d 6907 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑂‘𝑝) = (((eval1‘𝑅) ↾ 𝑈)‘𝑝)) | 
| 69 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈) | 
| 70 | 69 | fvresd 6925 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (((eval1‘𝑅) ↾ 𝑈)‘𝑝) = ((eval1‘𝑅)‘𝑝)) | 
| 71 | 68, 70 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑂‘𝑝) = ((eval1‘𝑅)‘𝑝)) | 
| 72 | 71 | fveq1d 6907 | . . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝑋) = (((eval1‘𝑅)‘𝑝)‘𝑋)) | 
| 73 |  | eqid 2736 | . . . . 5
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) | 
| 74 |  | eqid 2736 | . . . . 5
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) | 
| 75 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑅 ∈ CRing) | 
| 76 | 38 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑋 ∈ 𝐵) | 
| 77 |  | eqid 2736 | . . . . . . . 8
⊢
(PwSer1‘(𝑅 ↾s 𝑆)) = (PwSer1‘(𝑅 ↾s 𝑆)) | 
| 78 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘(PwSer1‘(𝑅 ↾s 𝑆))) =
(Base‘(PwSer1‘(𝑅 ↾s 𝑆))) | 
| 79 | 73, 8, 11, 1, 7, 77, 78, 74 | ressply1bas2 22230 | . . . . . . 7
⊢ (𝜑 → 𝑈 =
((Base‘(PwSer1‘(𝑅 ↾s 𝑆))) ∩
(Base‘(Poly1‘𝑅)))) | 
| 80 |  | inss2 4237 | . . . . . . 7
⊢
((Base‘(PwSer1‘(𝑅 ↾s 𝑆))) ∩
(Base‘(Poly1‘𝑅))) ⊆
(Base‘(Poly1‘𝑅)) | 
| 81 | 79, 80 | eqsstrdi 4027 | . . . . . 6
⊢ (𝜑 → 𝑈 ⊆
(Base‘(Poly1‘𝑅))) | 
| 82 | 81 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈
(Base‘(Poly1‘𝑅))) | 
| 83 | 65, 73, 35, 74, 75, 76, 82 | fveval1fvcl 22338 | . . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (((eval1‘𝑅)‘𝑝)‘𝑋) ∈ 𝐵) | 
| 84 | 72, 83 | eqeltrd 2840 | . . 3
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝑋) ∈ 𝐵) | 
| 85 | 84, 16 | fmptd 7133 | . 2
⊢ (𝜑 → 𝐹:𝑈⟶𝐵) | 
| 86 | 34, 35, 11, 8, 1, 63, 64, 41, 42, 43, 44, 45 | evls1addd 22376 | . . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋) = (((𝑂‘𝑞)‘𝑋)(+g‘𝑅)((𝑂‘𝑟)‘𝑋))) | 
| 87 |  | fveq2 6905 | . . . . 5
⊢ (𝑝 = (𝑞(+g‘𝑃)𝑟) → (𝑂‘𝑝) = (𝑂‘(𝑞(+g‘𝑃)𝑟))) | 
| 88 | 87 | fveq1d 6907 | . . . 4
⊢ (𝑝 = (𝑞(+g‘𝑃)𝑟) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋)) | 
| 89 | 49 | ringgrpd 20240 | . . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑃 ∈ Grp) | 
| 90 | 1, 63, 89, 43, 44 | grpcld 18966 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝑞(+g‘𝑃)𝑟) ∈ 𝑈) | 
| 91 |  | fvexd 6920 | . . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋) ∈ V) | 
| 92 | 16, 88, 90, 91 | fvmptd3 7038 | . . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(+g‘𝑃)𝑟)) = ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋)) | 
| 93 | 56, 60 | oveq12d 7450 | . . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝐹‘𝑞)(+g‘𝑅)(𝐹‘𝑟)) = (((𝑂‘𝑞)‘𝑋)(+g‘𝑅)((𝑂‘𝑟)‘𝑋))) | 
| 94 | 86, 92, 93 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(+g‘𝑃)𝑟)) = ((𝐹‘𝑞)(+g‘𝑅)(𝐹‘𝑟))) | 
| 95 | 1, 2, 3, 4, 5, 14,
15, 40, 62, 35, 63, 64, 85, 94 | isrhmd 20489 | 1
⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) |