Step | Hyp | Ref
| Expression |
1 | | evls1maprhm.u |
. 2
⊢ 𝑈 = (Base‘𝑃) |
2 | | eqid 2731 |
. 2
⊢
(1r‘𝑃) = (1r‘𝑃) |
3 | | eqid 2731 |
. 2
⊢
(1r‘𝑅) = (1r‘𝑅) |
4 | | eqid 2731 |
. 2
⊢
(.r‘𝑃) = (.r‘𝑃) |
5 | | eqid 2731 |
. 2
⊢
(.r‘𝑅) = (.r‘𝑅) |
6 | | evls1maprhm.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
7 | | evls1maprhm.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |
8 | | eqid 2731 |
. . . . . 6
⊢ (𝑅 ↾s 𝑆) = (𝑅 ↾s 𝑆) |
9 | 8 | subrgcrng 20473 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ (SubRing‘𝑅)) → (𝑅 ↾s 𝑆) ∈ CRing) |
10 | 6, 7, 9 | syl2anc 583 |
. . . 4
⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ CRing) |
11 | | evls1maprhm.p |
. . . . 5
⊢ 𝑃 =
(Poly1‘(𝑅
↾s 𝑆)) |
12 | 11 | ply1crng 22040 |
. . . 4
⊢ ((𝑅 ↾s 𝑆) ∈ CRing → 𝑃 ∈ CRing) |
13 | 10, 12 | syl 17 |
. . 3
⊢ (𝜑 → 𝑃 ∈ CRing) |
14 | 13 | crngringd 20147 |
. 2
⊢ (𝜑 → 𝑃 ∈ Ring) |
15 | 6 | crngringd 20147 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
16 | | evls1maprhm.f |
. . . 4
⊢ 𝐹 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝑋)) |
17 | | fveq2 6891 |
. . . . 5
⊢ (𝑝 = (1r‘𝑃) → (𝑂‘𝑝) = (𝑂‘(1r‘𝑃))) |
18 | 17 | fveq1d 6893 |
. . . 4
⊢ (𝑝 = (1r‘𝑃) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(1r‘𝑃))‘𝑋)) |
19 | 1, 2 | ringidcl 20161 |
. . . . 5
⊢ (𝑃 ∈ Ring →
(1r‘𝑃)
∈ 𝑈) |
20 | 14, 19 | syl 17 |
. . . 4
⊢ (𝜑 → (1r‘𝑃) ∈ 𝑈) |
21 | | fvexd 6906 |
. . . 4
⊢ (𝜑 → ((𝑂‘(1r‘𝑃))‘𝑋) ∈ V) |
22 | 16, 18, 20, 21 | fvmptd3 7021 |
. . 3
⊢ (𝜑 → (𝐹‘(1r‘𝑃)) = ((𝑂‘(1r‘𝑃))‘𝑋)) |
23 | 8, 3 | subrg1 20480 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘(𝑅
↾s 𝑆))) |
24 | 7, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑅) = (1r‘(𝑅 ↾s 𝑆))) |
25 | 24 | fveq2d 6895 |
. . . . . 6
⊢ (𝜑 → ((algSc‘𝑃)‘(1r‘𝑅)) = ((algSc‘𝑃)‘(1r‘(𝑅 ↾s 𝑆)))) |
26 | 10 | crngringd 20147 |
. . . . . . 7
⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Ring) |
27 | | eqid 2731 |
. . . . . . . 8
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
28 | | eqid 2731 |
. . . . . . . 8
⊢
(1r‘(𝑅 ↾s 𝑆)) = (1r‘(𝑅 ↾s 𝑆)) |
29 | 11, 27, 28, 2 | ply1scl1 22134 |
. . . . . . 7
⊢ ((𝑅 ↾s 𝑆) ∈ Ring →
((algSc‘𝑃)‘(1r‘(𝑅 ↾s 𝑆))) = (1r‘𝑃)) |
30 | 26, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((algSc‘𝑃)‘(1r‘(𝑅 ↾s 𝑆))) = (1r‘𝑃)) |
31 | 25, 30 | eqtr2d 2772 |
. . . . 5
⊢ (𝜑 → (1r‘𝑃) = ((algSc‘𝑃)‘(1r‘𝑅))) |
32 | 31 | fveq2d 6895 |
. . . 4
⊢ (𝜑 → (𝑂‘(1r‘𝑃)) = (𝑂‘((algSc‘𝑃)‘(1r‘𝑅)))) |
33 | 32 | fveq1d 6893 |
. . 3
⊢ (𝜑 → ((𝑂‘(1r‘𝑃))‘𝑋) = ((𝑂‘((algSc‘𝑃)‘(1r‘𝑅)))‘𝑋)) |
34 | | evls1maprhm.q |
. . . 4
⊢ 𝑂 = (𝑅 evalSub1 𝑆) |
35 | | evls1maprhm.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
36 | 3 | subrg1cl 20478 |
. . . . 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 33082 |
. . 3
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘(1r‘𝑅)))‘𝑋) = (1r‘𝑅)) |
40 | 22, 33, 39 | 3eqtrd 2775 |
. 2
⊢ (𝜑 → (𝐹‘(1r‘𝑃)) = (1r‘𝑅)) |
41 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑅 ∈ CRing) |
42 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑆 ∈ (SubRing‘𝑅)) |
43 | | simprl 768 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑞 ∈ 𝑈) |
44 | | simprr 770 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑟 ∈ 𝑈) |
45 | 38 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑋 ∈ 𝐵) |
46 | 34, 35, 11, 8, 1, 4,
5, 41, 42, 43, 44, 45 | evls1muld 33088 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋) = (((𝑂‘𝑞)‘𝑋)(.r‘𝑅)((𝑂‘𝑟)‘𝑋))) |
47 | | fveq2 6891 |
. . . . 5
⊢ (𝑝 = (𝑞(.r‘𝑃)𝑟) → (𝑂‘𝑝) = (𝑂‘(𝑞(.r‘𝑃)𝑟))) |
48 | 47 | fveq1d 6893 |
. . . 4
⊢ (𝑝 = (𝑞(.r‘𝑃)𝑟) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋)) |
49 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑃 ∈ Ring) |
50 | 1, 4, 49, 43, 44 | ringcld 20158 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝑞(.r‘𝑃)𝑟) ∈ 𝑈) |
51 | | fvexd 6906 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋) ∈ V) |
52 | 16, 48, 50, 51 | fvmptd3 7021 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(.r‘𝑃)𝑟)) = ((𝑂‘(𝑞(.r‘𝑃)𝑟))‘𝑋)) |
53 | | fveq2 6891 |
. . . . . 6
⊢ (𝑝 = 𝑞 → (𝑂‘𝑝) = (𝑂‘𝑞)) |
54 | 53 | fveq1d 6893 |
. . . . 5
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘𝑞)‘𝑋)) |
55 | | fvexd 6906 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘𝑞)‘𝑋) ∈ V) |
56 | 16, 54, 43, 55 | fvmptd3 7021 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘𝑞) = ((𝑂‘𝑞)‘𝑋)) |
57 | | fveq2 6891 |
. . . . . 6
⊢ (𝑝 = 𝑟 → (𝑂‘𝑝) = (𝑂‘𝑟)) |
58 | 57 | fveq1d 6893 |
. . . . 5
⊢ (𝑝 = 𝑟 → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘𝑟)‘𝑋)) |
59 | | fvexd 6906 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘𝑟)‘𝑋) ∈ V) |
60 | 16, 58, 44, 59 | fvmptd3 7021 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘𝑟) = ((𝑂‘𝑟)‘𝑋)) |
61 | 56, 60 | oveq12d 7430 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝐹‘𝑞)(.r‘𝑅)(𝐹‘𝑟)) = (((𝑂‘𝑞)‘𝑋)(.r‘𝑅)((𝑂‘𝑟)‘𝑋))) |
62 | 46, 52, 61 | 3eqtr4d 2781 |
. 2
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(.r‘𝑃)𝑟)) = ((𝐹‘𝑞)(.r‘𝑅)(𝐹‘𝑟))) |
63 | | eqid 2731 |
. 2
⊢
(+g‘𝑃) = (+g‘𝑃) |
64 | | eqid 2731 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
65 | | eqid 2731 |
. . . . . . . . 9
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
66 | 34, 35, 11, 8, 1, 65, 6, 7 | ressply1evl 33086 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 = ((eval1‘𝑅) ↾ 𝑈)) |
67 | 66 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑂 = ((eval1‘𝑅) ↾ 𝑈)) |
68 | 67 | fveq1d 6893 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑂‘𝑝) = (((eval1‘𝑅) ↾ 𝑈)‘𝑝)) |
69 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈) |
70 | 69 | fvresd 6911 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (((eval1‘𝑅) ↾ 𝑈)‘𝑝) = ((eval1‘𝑅)‘𝑝)) |
71 | 68, 70 | eqtrd 2771 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑂‘𝑝) = ((eval1‘𝑅)‘𝑝)) |
72 | 71 | fveq1d 6893 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝑋) = (((eval1‘𝑅)‘𝑝)‘𝑋)) |
73 | | eqid 2731 |
. . . . 5
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
74 | | eqid 2731 |
. . . . 5
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
75 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑅 ∈ CRing) |
76 | 38 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑋 ∈ 𝐵) |
77 | | eqid 2731 |
. . . . . . . 8
⊢
(PwSer1‘(𝑅 ↾s 𝑆)) = (PwSer1‘(𝑅 ↾s 𝑆)) |
78 | | eqid 2731 |
. . . . . . . 8
⊢
(Base‘(PwSer1‘(𝑅 ↾s 𝑆))) =
(Base‘(PwSer1‘(𝑅 ↾s 𝑆))) |
79 | 73, 8, 11, 1, 7, 77, 78, 74 | ressply1bas2 22069 |
. . . . . . 7
⊢ (𝜑 → 𝑈 =
((Base‘(PwSer1‘(𝑅 ↾s 𝑆))) ∩
(Base‘(Poly1‘𝑅)))) |
80 | | inss2 4229 |
. . . . . . 7
⊢
((Base‘(PwSer1‘(𝑅 ↾s 𝑆))) ∩
(Base‘(Poly1‘𝑅))) ⊆
(Base‘(Poly1‘𝑅)) |
81 | 79, 80 | eqsstrdi 4036 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆
(Base‘(Poly1‘𝑅))) |
82 | 81 | sselda 3982 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈
(Base‘(Poly1‘𝑅))) |
83 | 65, 73, 35, 74, 75, 76, 82 | fveval1fvcl 22171 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (((eval1‘𝑅)‘𝑝)‘𝑋) ∈ 𝐵) |
84 | 72, 83 | eqeltrd 2832 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝑋) ∈ 𝐵) |
85 | 84, 16 | fmptd 7115 |
. 2
⊢ (𝜑 → 𝐹:𝑈⟶𝐵) |
86 | 34, 35, 11, 8, 1, 63, 64, 41, 42, 43, 44, 45 | evls1addd 33087 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋) = (((𝑂‘𝑞)‘𝑋)(+g‘𝑅)((𝑂‘𝑟)‘𝑋))) |
87 | | fveq2 6891 |
. . . . 5
⊢ (𝑝 = (𝑞(+g‘𝑃)𝑟) → (𝑂‘𝑝) = (𝑂‘(𝑞(+g‘𝑃)𝑟))) |
88 | 87 | fveq1d 6893 |
. . . 4
⊢ (𝑝 = (𝑞(+g‘𝑃)𝑟) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋)) |
89 | 49 | ringgrpd 20143 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → 𝑃 ∈ Grp) |
90 | 1, 63, 89, 43, 44 | grpcld 18875 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝑞(+g‘𝑃)𝑟) ∈ 𝑈) |
91 | | fvexd 6906 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋) ∈ V) |
92 | 16, 88, 90, 91 | fvmptd3 7021 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(+g‘𝑃)𝑟)) = ((𝑂‘(𝑞(+g‘𝑃)𝑟))‘𝑋)) |
93 | 56, 60 | oveq12d 7430 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → ((𝐹‘𝑞)(+g‘𝑅)(𝐹‘𝑟)) = (((𝑂‘𝑞)‘𝑋)(+g‘𝑅)((𝑂‘𝑟)‘𝑋))) |
94 | 86, 92, 93 | 3eqtr4d 2781 |
. 2
⊢ ((𝜑 ∧ (𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈)) → (𝐹‘(𝑞(+g‘𝑃)𝑟)) = ((𝐹‘𝑞)(+g‘𝑅)(𝐹‘𝑟))) |
95 | 1, 2, 3, 4, 5, 14,
15, 40, 62, 35, 63, 64, 85, 94 | isrhmd 20386 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) |