Step | Hyp | Ref
| Expression |
1 | | evlsmaprhm.b |
. 2
⊢ 𝐵 = (Base‘𝑃) |
2 | | eqid 2724 |
. 2
⊢
(1r‘𝑃) = (1r‘𝑃) |
3 | | eqid 2724 |
. 2
⊢
(1r‘𝑅) = (1r‘𝑅) |
4 | | eqid 2724 |
. 2
⊢
(.r‘𝑃) = (.r‘𝑃) |
5 | | eqid 2724 |
. 2
⊢
(.r‘𝑅) = (.r‘𝑅) |
6 | | evlsmaprhm.p |
. . 3
⊢ 𝑃 = (𝐼 mPoly 𝑈) |
7 | | evlsmaprhm.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
8 | | evlsmaprhm.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |
9 | | evlsmaprhm.u |
. . . . 5
⊢ 𝑈 = (𝑅 ↾s 𝑆) |
10 | 9 | subrgring 20461 |
. . . 4
⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑈 ∈ Ring) |
11 | 8, 10 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ∈ Ring) |
12 | 6, 7, 11 | mplringd 41572 |
. 2
⊢ (𝜑 → 𝑃 ∈ Ring) |
13 | | evlsmaprhm.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
14 | 13 | crngringd 20136 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
15 | | evlsmaprhm.f |
. . . 4
⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴)) |
16 | | fveq2 6881 |
. . . . 5
⊢ (𝑝 = (1r‘𝑃) → (𝑄‘𝑝) = (𝑄‘(1r‘𝑃))) |
17 | 16 | fveq1d 6883 |
. . . 4
⊢ (𝑝 = (1r‘𝑃) → ((𝑄‘𝑝)‘𝐴) = ((𝑄‘(1r‘𝑃))‘𝐴)) |
18 | 1, 2 | ringidcl 20150 |
. . . . 5
⊢ (𝑃 ∈ Ring →
(1r‘𝑃)
∈ 𝐵) |
19 | 12, 18 | syl 17 |
. . . 4
⊢ (𝜑 → (1r‘𝑃) ∈ 𝐵) |
20 | | fvexd 6896 |
. . . 4
⊢ (𝜑 → ((𝑄‘(1r‘𝑃))‘𝐴) ∈ V) |
21 | 15, 17, 19, 20 | fvmptd3 7011 |
. . 3
⊢ (𝜑 → (𝐹‘(1r‘𝑃)) = ((𝑄‘(1r‘𝑃))‘𝐴)) |
22 | | eqid 2724 |
. . . . . . 7
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
23 | | eqid 2724 |
. . . . . . 7
⊢
(1r‘𝑈) = (1r‘𝑈) |
24 | 6, 22, 23, 2, 7, 11 | mplascl1 41582 |
. . . . . 6
⊢ (𝜑 → ((algSc‘𝑃)‘(1r‘𝑈)) = (1r‘𝑃)) |
25 | 24 | eqcomd 2730 |
. . . . 5
⊢ (𝜑 → (1r‘𝑃) = ((algSc‘𝑃)‘(1r‘𝑈))) |
26 | 25 | fveq2d 6885 |
. . . 4
⊢ (𝜑 → (𝑄‘(1r‘𝑃)) = (𝑄‘((algSc‘𝑃)‘(1r‘𝑈)))) |
27 | 26 | fveq1d 6883 |
. . 3
⊢ (𝜑 → ((𝑄‘(1r‘𝑃))‘𝐴) = ((𝑄‘((algSc‘𝑃)‘(1r‘𝑈)))‘𝐴)) |
28 | | evlsmaprhm.q |
. . . . . 6
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆) |
29 | | evlsmaprhm.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝑅) |
30 | 9, 3 | subrg1 20469 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘𝑈)) |
31 | 8, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑅) = (1r‘𝑈)) |
32 | 3 | subrg1cl 20467 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(1r‘𝑅)
∈ 𝑆) |
33 | 8, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆) |
34 | 31, 33 | eqeltrrd 2826 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑈) ∈ 𝑆) |
35 | | evlsmaprhm.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
36 | 28, 6, 9, 29, 1, 22, 7, 13, 8, 34, 35 | evlsscaval 41591 |
. . . . 5
⊢ (𝜑 → (((algSc‘𝑃)‘(1r‘𝑈)) ∈ 𝐵 ∧ ((𝑄‘((algSc‘𝑃)‘(1r‘𝑈)))‘𝐴) = (1r‘𝑈))) |
37 | 36 | simprd 495 |
. . . 4
⊢ (𝜑 → ((𝑄‘((algSc‘𝑃)‘(1r‘𝑈)))‘𝐴) = (1r‘𝑈)) |
38 | 37, 31 | eqtr4d 2767 |
. . 3
⊢ (𝜑 → ((𝑄‘((algSc‘𝑃)‘(1r‘𝑈)))‘𝐴) = (1r‘𝑅)) |
39 | 21, 27, 38 | 3eqtrd 2768 |
. 2
⊢ (𝜑 → (𝐹‘(1r‘𝑃)) = (1r‘𝑅)) |
40 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝐼 ∈ 𝑉) |
41 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑅 ∈ CRing) |
42 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑆 ∈ (SubRing‘𝑅)) |
43 | 35 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
44 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑞 ∈ 𝐵) |
45 | | eqidd 2725 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘𝑞)‘𝐴) = ((𝑄‘𝑞)‘𝐴)) |
46 | 44, 45 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝑞 ∈ 𝐵 ∧ ((𝑄‘𝑞)‘𝐴) = ((𝑄‘𝑞)‘𝐴))) |
47 | | simprr 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑟 ∈ 𝐵) |
48 | | eqidd 2725 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘𝑟)‘𝐴) = ((𝑄‘𝑟)‘𝐴)) |
49 | 47, 48 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝑟 ∈ 𝐵 ∧ ((𝑄‘𝑟)‘𝐴) = ((𝑄‘𝑟)‘𝐴))) |
50 | 28, 6, 9, 29, 1, 40, 41, 42, 43, 46, 49, 4, 5 | evlsmulval 41596 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑞(.r‘𝑃)𝑟) ∈ 𝐵 ∧ ((𝑄‘(𝑞(.r‘𝑃)𝑟))‘𝐴) = (((𝑄‘𝑞)‘𝐴)(.r‘𝑅)((𝑄‘𝑟)‘𝐴)))) |
51 | 50 | simprd 495 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘(𝑞(.r‘𝑃)𝑟))‘𝐴) = (((𝑄‘𝑞)‘𝐴)(.r‘𝑅)((𝑄‘𝑟)‘𝐴))) |
52 | | fveq2 6881 |
. . . . 5
⊢ (𝑝 = (𝑞(.r‘𝑃)𝑟) → (𝑄‘𝑝) = (𝑄‘(𝑞(.r‘𝑃)𝑟))) |
53 | 52 | fveq1d 6883 |
. . . 4
⊢ (𝑝 = (𝑞(.r‘𝑃)𝑟) → ((𝑄‘𝑝)‘𝐴) = ((𝑄‘(𝑞(.r‘𝑃)𝑟))‘𝐴)) |
54 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑃 ∈ Ring) |
55 | 1, 4, 54, 44, 47 | ringcld 20147 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝑞(.r‘𝑃)𝑟) ∈ 𝐵) |
56 | | fvexd 6896 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘(𝑞(.r‘𝑃)𝑟))‘𝐴) ∈ V) |
57 | 15, 53, 55, 56 | fvmptd3 7011 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝐹‘(𝑞(.r‘𝑃)𝑟)) = ((𝑄‘(𝑞(.r‘𝑃)𝑟))‘𝐴)) |
58 | | fveq2 6881 |
. . . . . 6
⊢ (𝑝 = 𝑞 → (𝑄‘𝑝) = (𝑄‘𝑞)) |
59 | 58 | fveq1d 6883 |
. . . . 5
⊢ (𝑝 = 𝑞 → ((𝑄‘𝑝)‘𝐴) = ((𝑄‘𝑞)‘𝐴)) |
60 | | fvexd 6896 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘𝑞)‘𝐴) ∈ V) |
61 | 15, 59, 44, 60 | fvmptd3 7011 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝐹‘𝑞) = ((𝑄‘𝑞)‘𝐴)) |
62 | | fveq2 6881 |
. . . . . 6
⊢ (𝑝 = 𝑟 → (𝑄‘𝑝) = (𝑄‘𝑟)) |
63 | 62 | fveq1d 6883 |
. . . . 5
⊢ (𝑝 = 𝑟 → ((𝑄‘𝑝)‘𝐴) = ((𝑄‘𝑟)‘𝐴)) |
64 | | fvexd 6896 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘𝑟)‘𝐴) ∈ V) |
65 | 15, 63, 47, 64 | fvmptd3 7011 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝐹‘𝑟) = ((𝑄‘𝑟)‘𝐴)) |
66 | 61, 65 | oveq12d 7419 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝐹‘𝑞)(.r‘𝑅)(𝐹‘𝑟)) = (((𝑄‘𝑞)‘𝐴)(.r‘𝑅)((𝑄‘𝑟)‘𝐴))) |
67 | 51, 57, 66 | 3eqtr4d 2774 |
. 2
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝐹‘(𝑞(.r‘𝑃)𝑟)) = ((𝐹‘𝑞)(.r‘𝑅)(𝐹‘𝑟))) |
68 | | eqid 2724 |
. 2
⊢
(+g‘𝑃) = (+g‘𝑃) |
69 | | eqid 2724 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
70 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
71 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing) |
72 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ (SubRing‘𝑅)) |
73 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵) |
74 | 35 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
75 | 28, 6, 9, 1, 29, 70, 71, 72, 73, 74 | evlscl 41585 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑄‘𝑝)‘𝐴) ∈ 𝐾) |
76 | 75, 15 | fmptd 7105 |
. 2
⊢ (𝜑 → 𝐹:𝐵⟶𝐾) |
77 | 28, 6, 9, 29, 1, 40, 41, 42, 43, 46, 49, 68, 69 | evlsaddval 41595 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑞(+g‘𝑃)𝑟) ∈ 𝐵 ∧ ((𝑄‘(𝑞(+g‘𝑃)𝑟))‘𝐴) = (((𝑄‘𝑞)‘𝐴)(+g‘𝑅)((𝑄‘𝑟)‘𝐴)))) |
78 | 77 | simprd 495 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘(𝑞(+g‘𝑃)𝑟))‘𝐴) = (((𝑄‘𝑞)‘𝐴)(+g‘𝑅)((𝑄‘𝑟)‘𝐴))) |
79 | | fveq2 6881 |
. . . . 5
⊢ (𝑝 = (𝑞(+g‘𝑃)𝑟) → (𝑄‘𝑝) = (𝑄‘(𝑞(+g‘𝑃)𝑟))) |
80 | 79 | fveq1d 6883 |
. . . 4
⊢ (𝑝 = (𝑞(+g‘𝑃)𝑟) → ((𝑄‘𝑝)‘𝐴) = ((𝑄‘(𝑞(+g‘𝑃)𝑟))‘𝐴)) |
81 | 12 | ringgrpd 20132 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Grp) |
82 | 81 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝑃 ∈ Grp) |
83 | 1, 68, 82, 44, 47 | grpcld 18864 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝑞(+g‘𝑃)𝑟) ∈ 𝐵) |
84 | | fvexd 6896 |
. . . 4
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑄‘(𝑞(+g‘𝑃)𝑟))‘𝐴) ∈ V) |
85 | 15, 80, 83, 84 | fvmptd3 7011 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝐹‘(𝑞(+g‘𝑃)𝑟)) = ((𝑄‘(𝑞(+g‘𝑃)𝑟))‘𝐴)) |
86 | 61, 65 | oveq12d 7419 |
. . 3
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝐹‘𝑞)(+g‘𝑅)(𝐹‘𝑟)) = (((𝑄‘𝑞)‘𝐴)(+g‘𝑅)((𝑄‘𝑟)‘𝐴))) |
87 | 78, 85, 86 | 3eqtr4d 2774 |
. 2
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → (𝐹‘(𝑞(+g‘𝑃)𝑟)) = ((𝐹‘𝑞)(+g‘𝑅)(𝐹‘𝑟))) |
88 | 1, 2, 3, 4, 5, 12,
14, 39, 67, 29, 68, 69, 76, 87 | isrhmd 20375 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) |