Step | Hyp | Ref
| Expression |
1 | | evlslem1.b |
. . 3
⊢ 𝐵 = (Base‘𝑃) |
2 | | eqid 2797 |
. . 3
⊢
(1r‘𝑃) = (1r‘𝑃) |
3 | | eqid 2797 |
. . 3
⊢
(1r‘𝑆) = (1r‘𝑆) |
4 | | eqid 2797 |
. . 3
⊢
(.r‘𝑃) = (.r‘𝑃) |
5 | | evlslem1.m |
. . 3
⊢ · =
(.r‘𝑆) |
6 | | evlslem1.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
7 | | evlslem1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
8 | | crngring 19002 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | | evlslem1.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
11 | 10 | mplring 19924 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
12 | 6, 9, 11 | syl2anc 584 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Ring) |
13 | | evlslem1.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) |
14 | | crngring 19002 |
. . . 4
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ∈ Ring) |
16 | | 2fveq3 6550 |
. . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅)))) |
17 | | fveq2 6545 |
. . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅))) |
18 | 16, 17 | eqeq12d 2812 |
. . . . 5
⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))) |
19 | | evlslem1.d |
. . . . . . . . 9
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
20 | | eqid 2797 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
21 | | eqid 2797 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
22 | | evlslem1.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
23 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐼 ∈ V) |
24 | 9 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
25 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
26 | 10, 19, 20, 21, 22, 23, 24, 25 | mplascl 19967 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) |
27 | 26 | fveq2d 6549 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))) |
28 | | evlslem1.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑆) |
29 | | evlslem1.t |
. . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) |
30 | | evlslem1.x |
. . . . . . . 8
⊢ ↑ =
(.g‘𝑇) |
31 | | evlslem1.v |
. . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) |
32 | | evlslem1.e |
. . . . . . . 8
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
33 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing) |
34 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing) |
35 | | evlslem1.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
36 | 35 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
37 | | evlslem1.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼⟶𝐶) |
39 | 19 | psrbag0 19965 |
. . . . . . . . . 10
⊢ (𝐼 ∈ V → (𝐼 × {0}) ∈ 𝐷) |
40 | 6, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) |
41 | 40 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷) |
42 | 10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 23, 33, 34, 36, 38, 20, 41, 25 | evlslem3 19984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)))) |
43 | | 0zd 11847 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ) |
44 | | fvexd 6560 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V) |
45 | | fconstmpt 5507 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)) |
47 | 37 | feqmptd 6608 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥))) |
48 | 6, 43, 44, 46, 47 | offval2 7291 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼 × {0}) ∘𝑓
↑
𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥)))) |
49 | 37 | ffvelrnda 6723 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶) |
50 | 29, 28 | mgpbas 18939 |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (Base‘𝑇) |
51 | 29, 3 | ringidval 18947 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (0g‘𝑇) |
52 | 50, 51, 30 | mulg0 17992 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) |
54 | 53 | mpteq2dva 5062 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) |
55 | 48, 54 | eqtrd 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐼 × {0}) ∘𝑓
↑
𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) |
56 | 55 | oveq2d 7039 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))) |
57 | 29 | crngmgp 18999 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
58 | 13, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ CMnd) |
59 | | cmnmnd 18652 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ Mnd) |
61 | 51 | gsumz 17817 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ V) → (𝑇 Σg
(𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) |
62 | 60, 6, 61 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) |
63 | 56, 62 | eqtrd 2833 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)) = (1r‘𝑆)) |
64 | 63 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)) = (1r‘𝑆)) |
65 | 64 | oveq2d 7039 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺))) = ((𝐹‘𝑥) ·
(1r‘𝑆))) |
66 | 21, 28 | rhmf 19172 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶) |
67 | 35, 66 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶) |
68 | 67 | ffvelrnda 6723 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ 𝐶) |
69 | 28, 5, 3 | ringridm 19016 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) |
70 | 15, 68, 69 | syl2an2r 681 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) |
71 | 65, 70 | eqtrd 2833 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺))) = (𝐹‘𝑥)) |
72 | 27, 42, 71 | 3eqtrd 2837 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) |
73 | 72 | ralrimiva 3151 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) |
74 | | eqid 2797 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
75 | 21, 74 | ringidcl 19012 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
76 | 9, 75 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
77 | 18, 73, 76 | rspcdva 3567 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))) |
78 | 10 | mplassa 19926 |
. . . . . . . . 9
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) |
79 | 6, 7, 78 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ AssAlg) |
80 | | eqid 2797 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
81 | 22, 80 | asclrhm 19811 |
. . . . . . . 8
⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
82 | 79, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
83 | 10, 6, 7 | mplsca 19917 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
84 | 83 | oveq1d 7038 |
. . . . . . 7
⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) |
85 | 82, 84 | eleqtrrd 2888 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃)) |
86 | 74, 2 | rhm1 19176 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) |
87 | 85, 86 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) |
88 | 87 | fveq2d 6549 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃))) |
89 | 74, 3 | rhm1 19176 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
90 | 35, 89 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
91 | 77, 88, 90 | 3eqtr3d 2841 |
. . 3
⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆)) |
92 | | eqid 2797 |
. . . . 5
⊢
(+g‘𝑃) = (+g‘𝑃) |
93 | | eqid 2797 |
. . . . 5
⊢
(+g‘𝑆) = (+g‘𝑆) |
94 | | ringgrp 18996 |
. . . . . 6
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
95 | 12, 94 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) |
96 | | ringgrp 18996 |
. . . . . 6
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
97 | 15, 96 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Grp) |
98 | | eqid 2797 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
99 | | ringcmn 19025 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd) |
100 | 15, 99 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CMnd) |
101 | 100 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd) |
102 | | ovex 7055 |
. . . . . . . . 9
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
103 | 19, 102 | rabex2 5135 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
104 | 103 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V) |
105 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ V) |
106 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing) |
107 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing) |
108 | 35 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
109 | 37 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶) |
110 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵) |
111 | 10, 1, 28, 19, 29, 30, 5, 31, 32, 105, 106, 107, 108, 109, 110 | evlslem6 19985 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |
112 | 111 | simpld 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
113 | 111 | simprd 496 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
114 | 28, 98, 101, 104, 112, 113 | gsumcl 18760 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈ 𝐶) |
115 | 114, 32 | fmptd 6748 |
. . . . 5
⊢ (𝜑 → 𝐸:𝐵⟶𝐶) |
116 | | eqid 2797 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝑅) = (+g‘𝑅) |
117 | | simplrl 773 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵) |
118 | | simplrr 774 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵) |
119 | 10, 1, 116, 92, 117, 118 | mpladd 19914 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘𝑓
(+g‘𝑅)𝑦)) |
120 | 119 | fveq1d 6547 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘𝑓
(+g‘𝑅)𝑦)‘𝑏)) |
121 | | simprl 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
122 | 10, 21, 1, 19, 121 | mplelf 19905 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶(Base‘𝑅)) |
123 | 122 | ffnd 6390 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷) |
124 | 123 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷) |
125 | | simprr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
126 | 10, 21, 1, 19, 125 | mplelf 19905 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶(Base‘𝑅)) |
127 | 126 | ffnd 6390 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷) |
129 | 103 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V) |
130 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
131 | | fnfvof 7288 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘𝑓
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
132 | 124, 128,
129, 130, 131 | syl22anc 835 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘𝑓
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
133 | 120, 132 | eqtrd 2833 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
134 | 133 | fveq2d 6549 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))) |
135 | | rhmghm 19171 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
136 | 35, 135 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
137 | 136 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
138 | 122 | ffvelrnda 6723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ (Base‘𝑅)) |
139 | 126 | ffvelrnda 6723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ (Base‘𝑅)) |
140 | 21, 116, 93 | ghmlin 18108 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ (Base‘𝑅) ∧ (𝑦‘𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
141 | 137, 138,
139, 140 | syl3anc 1364 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
142 | 134, 141 | eqtrd 2833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
143 | 142 | oveq1d 7038 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
144 | 15 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
145 | 67 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶) |
146 | 145, 138 | ffvelrnd 6724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶) |
147 | 145, 139 | ffvelrnd 6724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶) |
148 | 58 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
149 | 37 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
150 | 6 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V) |
151 | 19, 50, 30, 148, 130, 149, 150 | psrbagev2 19982 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
152 | 28, 93, 5 | ringdir 19011 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
153 | 144, 146,
147, 151, 152 | syl13anc 1365 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
154 | 143, 153 | eqtrd 2833 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
155 | 154 | mpteq2dva 5062 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
156 | 103 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V) |
157 | | ovexd 7057 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈
V) |
158 | | ovexd 7057 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈
V) |
159 | | eqidd 2798 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
160 | | eqidd 2798 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
161 | 156, 157,
158, 159, 160 | offval2 7291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
162 | 155, 161 | eqtr4d 2836 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
163 | 162 | oveq2d 7039 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
164 | 100 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd) |
165 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ V) |
166 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing) |
167 | 13 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing) |
168 | 35 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
169 | 37 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶) |
170 | 10, 1, 28, 19, 29, 30, 5, 31, 32, 165, 166, 167, 168, 169, 121 | evlslem6 19985 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |
171 | 170 | simpld 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
172 | 10, 1, 28, 19, 29, 30, 5, 31, 32, 165, 166, 167, 168, 169, 125 | evlslem6 19985 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |
173 | 172 | simpld 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
174 | 170 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
175 | 172 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
176 | 28, 98, 93, 164, 156, 171, 173, 174, 175 | gsumadd 18767 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) = ((𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
177 | 163, 176 | eqtrd 2833 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = ((𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
178 | 95 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp) |
179 | 1, 92 | grpcl 17873 |
. . . . . . . 8
⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) |
180 | 178, 121,
125, 179 | syl3anc 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) |
181 | | fveq1 6544 |
. . . . . . . . . . . 12
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏)) |
182 | 181 | fveq2d 6549 |
. . . . . . . . . . 11
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏))) |
183 | 182 | oveq1d 7038 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
184 | 183 | mpteq2dv 5063 |
. . . . . . . . 9
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
185 | 184 | oveq2d 7039 |
. . . . . . . 8
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
186 | | ovex 7055 |
. . . . . . . 8
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
187 | 185, 32, 186 | fvmpt 6642 |
. . . . . . 7
⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
188 | 180, 187 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
189 | | fveq1 6544 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏)) |
190 | 189 | fveq2d 6549 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏))) |
191 | 190 | oveq1d 7038 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
192 | 191 | mpteq2dv 5063 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
193 | 192 | oveq2d 7039 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
194 | | ovex 7055 |
. . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
195 | 193, 32, 194 | fvmpt 6642 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
196 | 121, 195 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
197 | | fveq1 6544 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏)) |
198 | 197 | fveq2d 6549 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏))) |
199 | 198 | oveq1d 7038 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
200 | 199 | mpteq2dv 5063 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
201 | 200 | oveq2d 7039 |
. . . . . . . . 9
⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
202 | | ovex 7055 |
. . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
203 | 201, 32, 202 | fvmpt 6642 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
204 | 203 | ad2antll 725 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
205 | 196, 204 | oveq12d 7041 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
206 | 177, 188,
205 | 3eqtr4d 2843 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦))) |
207 | 1, 28, 92, 93, 95, 97, 115, 206 | isghmd 18112 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆)) |
208 | | eqid 2797 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
209 | 208, 29 | rhmmhm 19168 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
210 | 35, 209 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
211 | 210 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
212 | | simprll 775 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵) |
213 | 10, 21, 1, 19, 212 | mplelf 19905 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶(Base‘𝑅)) |
214 | | simprrl 777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷) |
215 | 213, 214 | ffvelrnd 6724 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ (Base‘𝑅)) |
216 | | simprlr 776 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵) |
217 | 10, 21, 1, 19, 216 | mplelf 19905 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶(Base‘𝑅)) |
218 | | simprrr 778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷) |
219 | 217, 218 | ffvelrnd 6724 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ (Base‘𝑅)) |
220 | 208, 21 | mgpbas 18939 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
221 | | eqid 2797 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
222 | 208, 221 | mgpplusg 18937 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
223 | 29, 5 | mgpplusg 18937 |
. . . . . . . . 9
⊢ · =
(+g‘𝑇) |
224 | 220, 222,
223 | mhmlin 17785 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) |
225 | 211, 215,
219, 224 | syl3anc 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) |
226 | 60 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd) |
227 | | simprl 767 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷) |
228 | 19 | psrbagf 19837 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0) |
229 | 6, 227, 228 | syl2an2r 681 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0) |
230 | 229 | ffvelrnda 6723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈
ℕ0) |
231 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷) |
232 | 19 | psrbagf 19837 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝑤 ∈ 𝐷) → 𝑤:𝐼⟶ℕ0) |
233 | 6, 231, 232 | syl2an2r 681 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0) |
234 | 233 | ffvelrnda 6723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈
ℕ0) |
235 | 37 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶) |
236 | 235 | ffvelrnda 6723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶) |
237 | 50, 30, 223 | mulgnn0dir 18015 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
238 | 226, 230,
234, 236, 237 | syl13anc 1365 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
239 | 238 | mpteq2dva 5062 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) |
240 | 6 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ V) |
241 | | ovexd 7057 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V) |
242 | | fvexd 6560 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V) |
243 | 229 | ffnd 6390 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼) |
244 | 233 | ffnd 6390 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼) |
245 | | inidm 4121 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
246 | | eqidd 2798 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣)) |
247 | | eqidd 2798 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣)) |
248 | 243, 244,
240, 240, 245, 246, 247 | offval 7281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣)))) |
249 | 37 | feqmptd 6608 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) |
250 | 249 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) |
251 | 240, 241,
242, 248, 250 | offval2 7291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 + 𝑤) ∘𝑓
↑
𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)))) |
252 | | ovexd 7057 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) |
253 | | ovexd 7057 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) |
254 | 37 | ffnd 6390 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 Fn 𝐼) |
255 | 254 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼) |
256 | | eqidd 2798 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣)) |
257 | 243, 255,
240, 240, 245, 246, 256 | offval 7281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣)))) |
258 | 244, 255,
240, 240, 245, 247, 256 | offval 7281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘𝑓 ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
259 | 240, 252,
253, 257, 258 | offval2 7291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 ↑ 𝐺) ∘𝑓
·
(𝑤
∘𝑓 ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) |
260 | 239, 251,
259 | 3eqtr4d 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 + 𝑤) ∘𝑓
↑
𝐺) = ((𝑧 ∘𝑓 ↑ 𝐺) ∘𝑓
·
(𝑤
∘𝑓 ↑ 𝐺))) |
261 | 260 | oveq2d 7039 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘𝑓
↑
𝐺)
∘𝑓 · (𝑤 ∘𝑓 ↑ 𝐺)))) |
262 | 58 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd) |
263 | 19, 50, 30, 51, 262, 227, 235, 240 | psrbagev1 19981 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆))) |
264 | 263 | simpld 495 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶) |
265 | 19, 50, 30, 51, 262, 231, 235, 240 | psrbagev1 19981 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆))) |
266 | 265 | simpld 495 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶) |
267 | 263 | simprd 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆)) |
268 | 265 | simprd 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆)) |
269 | 50, 51, 223, 262, 240, 264, 266, 267, 268 | gsumadd 18767 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘𝑓
↑
𝐺)
∘𝑓 · (𝑤 ∘𝑓 ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
270 | 261, 269 | eqtrd 2833 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
271 | 270 | adantrl 712 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
272 | 225, 271 | oveq12d 7041 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
273 | 58 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd) |
274 | 67 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶) |
275 | 274, 215 | ffvelrnd 6724 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶) |
276 | 274, 219 | ffvelrnd 6724 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) |
277 | 19, 50, 30, 262, 227, 235, 240 | psrbagev2 19982 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
278 | 277 | adantrl 712 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
279 | 19, 50, 30, 262, 231, 235, 240 | psrbagev2 19982 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
280 | 279 | adantrl 712 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
281 | 50, 223 | cmn4 18656 |
. . . . . . 7
⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
282 | 273, 275,
276, 278, 280, 281 | syl122anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
283 | 272, 282 | eqtrd 2833 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
284 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ V) |
285 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing) |
286 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing) |
287 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
288 | 37 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶) |
289 | 19 | psrbagaddcl 19842 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘𝑓 + 𝑤) ∈ 𝐷) |
290 | 284, 214,
218, 289 | syl3anc 1364 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘𝑓 + 𝑤) ∈ 𝐷) |
291 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring) |
292 | 21, 221 | ringcl 19005 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) |
293 | 291, 215,
219, 292 | syl3anc 1364 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) |
294 | 10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 290, 293 | evlslem3 19984 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘𝑓 + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)))) |
295 | 10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 214, 215 | evlslem3 19984 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) = ((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)))) |
296 | 10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 218, 219 | evlslem3 19984 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
297 | 295, 296 | oveq12d 7041 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
298 | 283, 294,
297 | 3eqtr4d 2843 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘𝑓 + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))))) |
299 | 10, 1, 5, 20, 19, 6, 7, 13, 207, 298 | evlslem2 19983 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦))) |
300 | 1, 2, 3, 4, 5, 12,
15, 91, 299, 28, 92, 93, 115, 206 | isrhmd 19175 |
. 2
⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆)) |
301 | | ovex 7055 |
. . . . . 6
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
302 | 301, 32 | fnmpti 6366 |
. . . . 5
⊢ 𝐸 Fn 𝐵 |
303 | 302 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 Fn 𝐵) |
304 | 21, 1 | rhmf 19172 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵) |
305 | 85, 304 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶𝐵) |
306 | 305 | ffnd 6390 |
. . . 4
⊢ (𝜑 → 𝐴 Fn (Base‘𝑅)) |
307 | 305 | frnd 6396 |
. . . 4
⊢ (𝜑 → ran 𝐴 ⊆ 𝐵) |
308 | | fnco 6342 |
. . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn (Base‘𝑅) ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn (Base‘𝑅)) |
309 | 303, 306,
307, 308 | syl3anc 1364 |
. . 3
⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn (Base‘𝑅)) |
310 | 67 | ffnd 6390 |
. . 3
⊢ (𝜑 → 𝐹 Fn (Base‘𝑅)) |
311 | | fvco2 6632 |
. . . . 5
⊢ ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) |
312 | 306, 311 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) |
313 | 312, 72 | eqtrd 2833 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
314 | 309, 310,
313 | eqfnfvd 6677 |
. 2
⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹) |
315 | 10, 31, 1, 6, 9 | mvrf2 19963 |
. . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) |
316 | 315 | ffnd 6390 |
. . . 4
⊢ (𝜑 → 𝑉 Fn 𝐼) |
317 | 315 | frnd 6396 |
. . . 4
⊢ (𝜑 → ran 𝑉 ⊆ 𝐵) |
318 | | fnco 6342 |
. . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼) |
319 | 303, 316,
317, 318 | syl3anc 1364 |
. . 3
⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼) |
320 | | fvco2 6632 |
. . . . 5
⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) |
321 | 316, 320 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) |
322 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ V) |
323 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) |
324 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
325 | 31, 19, 20, 74, 322, 323, 324 | mvrval 19893 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) |
326 | 325 | fveq2d 6549 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))) |
327 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing) |
328 | 35 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
329 | 37 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶) |
330 | 19 | psrbagsn 19966 |
. . . . . . . 8
⊢ (𝐼 ∈ V → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
331 | 6, 330 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
332 | 331 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
333 | 76 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ (Base‘𝑅)) |
334 | 10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 322, 323, 327, 328, 329, 20, 332, 333 | evlslem3 19984 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺)))) |
335 | 90 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
336 | | 1nn0 11767 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
337 | | 0nn0 11766 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
338 | 336, 337 | ifcli 4433 |
. . . . . . . . . . . . 13
⊢ if(𝑧 = 𝑥, 1, 0) ∈
ℕ0 |
339 | 338 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈
ℕ0) |
340 | 37 | ffvelrnda 6723 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) |
341 | | eqidd 2798 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) |
342 | 37 | feqmptd 6608 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧))) |
343 | 6, 339, 340, 341, 342 | offval2 7291 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))) |
344 | | oveq1 7030 |
. . . . . . . . . . . . . 14
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) |
345 | 344 | eqeq1d 2799 |
. . . . . . . . . . . . 13
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
346 | | oveq1 7030 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) |
347 | 346 | eqeq1d 2799 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
348 | 340 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶) |
349 | 50, 30 | mulg1 17994 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) |
350 | 348, 349 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) |
351 | | iftrue 4393 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) |
352 | 351 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) |
353 | 350, 352 | eqtr4d 2836 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
354 | 50, 51, 30 | mulg0 17992 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
355 | 340, 354 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
356 | 355 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
357 | | iffalse 4396 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
358 | 357 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
359 | 356, 358 | eqtr4d 2836 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
360 | 345, 347,
353, 359 | ifbothda 4424 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
361 | 360 | mpteq2dva 5062 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
362 | 343, 361 | eqtrd 2833 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
363 | 362 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
364 | 363 | oveq2d 7039 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))) |
365 | 60 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd) |
366 | 340 | adantlr 711 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) |
367 | 28, 3 | ringidcl 19012 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝐶) |
368 | 15, 367 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶) |
369 | 368 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶) |
370 | 366, 369 | ifcld 4432 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶) |
371 | 370 | fmpttd 6749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶) |
372 | | eldifsnneq 4636 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥) |
373 | 372, 357 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
374 | 373 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
375 | 374, 322 | suppss2 7722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥}) |
376 | 50, 51, 365, 322, 324, 371, 375 | gsumpt 18806 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥)) |
377 | | fveq2 6545 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥)) |
378 | 351, 377 | eqtrd 2833 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥)) |
379 | | eqid 2797 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
380 | | fvex 6558 |
. . . . . . . . . 10
⊢ (𝐺‘𝑥) ∈ V |
381 | 378, 379,
380 | fvmpt 6642 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) |
382 | 381 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) |
383 | 364, 376,
382 | 3eqtrd 2837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺)) = (𝐺‘𝑥)) |
384 | 335, 383 | oveq12d 7041 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺))) =
((1r‘𝑆)
·
(𝐺‘𝑥))) |
385 | 28, 5, 3 | ringlidm 19015 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) |
386 | 15, 49, 385 | syl2an2r 681 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) |
387 | 384, 386 | eqtrd 2833 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺))) = (𝐺‘𝑥)) |
388 | 326, 334,
387 | 3eqtrd 2837 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥)) |
389 | 321, 388 | eqtrd 2833 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥)) |
390 | 319, 254,
389 | eqfnfvd 6677 |
. 2
⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺) |
391 | 300, 314,
390 | 3jca 1121 |
1
⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺)) |