Step | Hyp | Ref
| Expression |
1 | | evlslem1.b |
. . 3
⊢ 𝐵 = (Base‘𝑃) |
2 | | eqid 2610 |
. . 3
⊢
(1r‘𝑃) = (1r‘𝑃) |
3 | | eqid 2610 |
. . 3
⊢
(1r‘𝑆) = (1r‘𝑆) |
4 | | eqid 2610 |
. . 3
⊢
(.r‘𝑃) = (.r‘𝑃) |
5 | | evlslem1.m |
. . 3
⊢ · =
(.r‘𝑆) |
6 | | evlslem1.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
7 | | evlslem1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
8 | | crngring 18381 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | | evlslem1.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
11 | 10 | mplring 19273 |
. . . 4
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
12 | 6, 9, 11 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Ring) |
13 | | evlslem1.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) |
14 | | crngring 18381 |
. . . 4
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ∈ Ring) |
16 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (1r‘𝑅) → (𝐴‘𝑥) = (𝐴‘(1r‘𝑅))) |
17 | 16 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅)))) |
18 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅))) |
19 | 17, 18 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))) |
20 | | evlslem1.d |
. . . . . . . . 9
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
21 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
22 | | evlslem1.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
23 | | evlslem1.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
24 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝐼 ∈ V) |
25 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ Ring) |
26 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) |
27 | 10, 20, 21, 22, 23, 24, 25, 26 | mplascl 19317 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) |
28 | 27 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))) |
29 | | evlslem1.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑆) |
30 | | evlslem1.t |
. . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) |
31 | | evlslem1.x |
. . . . . . . 8
⊢ ↑ =
(.g‘𝑇) |
32 | | evlslem1.v |
. . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) |
33 | | evlslem1.e |
. . . . . . . 8
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
34 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ CRing) |
35 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑆 ∈ CRing) |
36 | | evlslem1.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
38 | | evlslem1.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
39 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝐺:𝐼⟶𝐶) |
40 | 20 | psrbag0 19315 |
. . . . . . . . . 10
⊢ (𝐼 ∈ V → (𝐼 × {0}) ∈ 𝐷) |
41 | 6, 40 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) |
42 | 41 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐼 × {0}) ∈ 𝐷) |
43 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 24, 34, 35, 37, 39, 21, 42, 26 | evlslem3 19335 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)))) |
44 | | 0zd 11266 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ) |
45 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘𝑥) ∈ V |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V) |
47 | | fconstmpt 5085 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)) |
49 | 38 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥))) |
50 | 6, 44, 46, 48, 49 | offval2 6812 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼 × {0}) ∘𝑓
↑
𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥)))) |
51 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶) |
52 | 30, 29 | mgpbas 18318 |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (Base‘𝑇) |
53 | 30, 3 | ringidval 18326 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (0g‘𝑇) |
54 | 52, 53, 31 | mulg0 17369 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) |
55 | 51, 54 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) |
56 | 55 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) |
57 | 50, 56 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐼 × {0}) ∘𝑓
↑
𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) |
58 | 57 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))) |
59 | 30 | crngmgp 18378 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
60 | 13, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ CMnd) |
61 | | cmnmnd 18031 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ Mnd) |
63 | 53 | gsumz 17197 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ V) → (𝑇 Σg
(𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) |
64 | 62, 6, 63 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) |
65 | 58, 64 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)) = (1r‘𝑆)) |
66 | 65 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺)) = (1r‘𝑆)) |
67 | 66 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺))) = ((𝐹‘𝑥) ·
(1r‘𝑆))) |
68 | 22, 29 | rhmf 18549 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶) |
69 | 36, 68 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐾⟶𝐶) |
70 | 69 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘𝑥) ∈ 𝐶) |
71 | 29, 5, 3 | ringridm 18395 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) |
72 | 15, 70, 71 | syl2an2r 872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) |
73 | 67, 72 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘𝑓 ↑ 𝐺))) = (𝐹‘𝑥)) |
74 | 28, 43, 73 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) |
75 | 74 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) |
76 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
77 | 22, 76 | ringidcl 18391 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐾) |
78 | 9, 77 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐾) |
79 | 19, 75, 78 | rspcdva 3288 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))) |
80 | 10 | mplassa 19275 |
. . . . . . . . 9
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) |
81 | 6, 7, 80 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ AssAlg) |
82 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
83 | 23, 82 | asclrhm 19163 |
. . . . . . . 8
⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
84 | 81, 83 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
85 | 10, 6, 7 | mplsca 19266 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
86 | 85 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) |
87 | 84, 86 | eleqtrrd 2691 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃)) |
88 | 76, 2 | rhm1 18553 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) |
89 | 87, 88 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) |
90 | 89 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃))) |
91 | 76, 3 | rhm1 18553 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
92 | 36, 91 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
93 | 79, 90, 92 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆)) |
94 | | eqid 2610 |
. . . . 5
⊢
(+g‘𝑃) = (+g‘𝑃) |
95 | | eqid 2610 |
. . . . 5
⊢
(+g‘𝑆) = (+g‘𝑆) |
96 | | ringgrp 18375 |
. . . . . 6
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
97 | 12, 96 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) |
98 | | ringgrp 18375 |
. . . . . 6
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
99 | 15, 98 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Grp) |
100 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
101 | | ringcmn 18404 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd) |
102 | 15, 101 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CMnd) |
103 | 102 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd) |
104 | | ovex 6577 |
. . . . . . . . 9
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
105 | 20, 104 | rabex2 4742 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
106 | 105 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V) |
107 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ V) |
108 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing) |
109 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing) |
110 | 36 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
111 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶) |
112 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵) |
113 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 107, 108, 109, 110, 111, 112 | evlslem6 19334 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |
114 | 113 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
115 | 113 | simprd 478 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
116 | 29, 100, 103, 106, 114, 115 | gsumcl 18139 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈ 𝐶) |
117 | 116, 33 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐸:𝐵⟶𝐶) |
118 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝑅) = (+g‘𝑅) |
119 | | simplrl 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵) |
120 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵) |
121 | 10, 1, 118, 94, 119, 120 | mpladd 19263 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘𝑓
(+g‘𝑅)𝑦)) |
122 | 121 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘𝑓
(+g‘𝑅)𝑦)‘𝑏)) |
123 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
124 | 10, 22, 1, 20, 123 | mplelf 19254 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶𝐾) |
125 | 124 | ffnd 5959 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷) |
126 | 125 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷) |
127 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
128 | 10, 22, 1, 20, 127 | mplelf 19254 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶𝐾) |
129 | 128 | ffnd 5959 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷) |
130 | 129 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷) |
131 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V) |
132 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
133 | | fnfvof 6809 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘𝑓
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
134 | 126, 130,
131, 132, 133 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘𝑓
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
135 | 122, 134 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
136 | 135 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))) |
137 | | rhmghm 18548 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
138 | 36, 137 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
139 | 138 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
140 | 124 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ 𝐾) |
141 | 128 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ 𝐾) |
142 | 22, 118, 95 | ghmlin 17488 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ 𝐾 ∧ (𝑦‘𝑏) ∈ 𝐾) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
143 | 139, 140,
141, 142 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
144 | 136, 143 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
145 | 144 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
146 | 15 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
147 | 69 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:𝐾⟶𝐶) |
148 | 147, 140 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶) |
149 | 147, 141 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶) |
150 | 60 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
151 | 38 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
152 | 6 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V) |
153 | 20, 52, 31, 53, 150, 132, 151, 152 | psrbagev2 19332 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
154 | 29, 95, 5 | ringdir 18390 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
155 | 146, 148,
149, 153, 154 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
156 | 145, 155 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
157 | 156 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
158 | 105 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V) |
159 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈
V |
160 | 159 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈
V) |
161 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈
V |
162 | 161 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈
V) |
163 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
164 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
165 | 158, 160,
162, 163, 164 | offval2 6812 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
166 | 157, 165 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
167 | 166 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
168 | 102 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd) |
169 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ V) |
170 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing) |
171 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing) |
172 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
173 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶) |
174 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 169, 170, 171, 172, 173, 123 | evlslem6 19334 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |
175 | 174 | simpld 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
176 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 169, 170, 171, 172, 173, 127 | evlslem6 19334 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆))) |
177 | 176 | simpld 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
178 | 174 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
179 | 176 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) finSupp
(0g‘𝑆)) |
180 | 29, 100, 95, 168, 158, 175, 177, 178, 179 | gsumadd 18146 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))
∘𝑓 (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) = ((𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
181 | 167, 180 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = ((𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
182 | 97 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp) |
183 | 1, 94 | grpcl 17253 |
. . . . . . . 8
⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) |
184 | 182, 123,
127, 183 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) |
185 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏)) |
186 | 185 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏))) |
187 | 186 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
188 | 187 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
189 | 188 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
190 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
191 | 189, 33, 190 | fvmpt 6191 |
. . . . . . 7
⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
192 | 184, 191 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
193 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏)) |
194 | 193 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏))) |
195 | 194 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
196 | 195 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
197 | 196 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
198 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
199 | 197, 33, 198 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
200 | 123, 199 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
201 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏)) |
202 | 201 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏))) |
203 | 202 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
204 | 203 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
205 | 204 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
206 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
207 | 205, 33, 206 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
208 | 207 | ad2antll 761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
209 | 200, 208 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))))) |
210 | 181, 192,
209 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦))) |
211 | 1, 29, 94, 95, 97, 99, 117, 210 | isghmd 17492 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆)) |
212 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
213 | 212, 30 | rhmmhm 18545 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
214 | 36, 213 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
215 | 214 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
216 | | simprll 798 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵) |
217 | 10, 22, 1, 20, 216 | mplelf 19254 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶𝐾) |
218 | | simprrl 800 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷) |
219 | 217, 218 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ 𝐾) |
220 | | simprlr 799 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵) |
221 | 10, 22, 1, 20, 220 | mplelf 19254 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶𝐾) |
222 | | simprrr 801 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷) |
223 | 221, 222 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ 𝐾) |
224 | 212, 22 | mgpbas 18318 |
. . . . . . . . 9
⊢ 𝐾 =
(Base‘(mulGrp‘𝑅)) |
225 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
226 | 212, 225 | mgpplusg 18316 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
227 | 30, 5 | mgpplusg 18316 |
. . . . . . . . 9
⊢ · =
(+g‘𝑇) |
228 | 224, 226,
227 | mhmlin 17165 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ 𝐾 ∧ (𝑦‘𝑤) ∈ 𝐾) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) |
229 | 215, 219,
223, 228 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) |
230 | 62 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd) |
231 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷) |
232 | 20 | psrbagf 19186 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0) |
233 | 6, 231, 232 | syl2an2r 872 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0) |
234 | 233 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈
ℕ0) |
235 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷) |
236 | 20 | psrbagf 19186 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝑤 ∈ 𝐷) → 𝑤:𝐼⟶ℕ0) |
237 | 6, 235, 236 | syl2an2r 872 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0) |
238 | 237 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈
ℕ0) |
239 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶) |
240 | 239 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶) |
241 | 52, 31, 227 | mulgnn0dir 17394 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
242 | 230, 234,
238, 240, 241 | syl13anc 1320 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
243 | 242 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) |
244 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ V) |
245 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V |
246 | 245 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V) |
247 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐺‘𝑣) ∈ V |
248 | 247 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V) |
249 | 233 | ffnd 5959 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼) |
250 | 237 | ffnd 5959 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼) |
251 | | inidm 3784 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
252 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣)) |
253 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣)) |
254 | 249, 250,
244, 244, 251, 252, 253 | offval 6802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣)))) |
255 | 38 | feqmptd 6159 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) |
256 | 255 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) |
257 | 244, 246,
248, 254, 256 | offval2 6812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 + 𝑤) ∘𝑓
↑
𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)))) |
258 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V |
259 | 258 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) |
260 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V |
261 | 260 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) |
262 | 38 | ffnd 5959 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 Fn 𝐼) |
263 | 262 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼) |
264 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣)) |
265 | 249, 263,
244, 244, 251, 252, 264 | offval 6802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣)))) |
266 | 250, 263,
244, 244, 251, 253, 264 | offval 6802 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘𝑓 ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
267 | 244, 259,
261, 265, 266 | offval2 6812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 ↑ 𝐺) ∘𝑓
·
(𝑤
∘𝑓 ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) |
268 | 243, 257,
267 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 + 𝑤) ∘𝑓
↑
𝐺) = ((𝑧 ∘𝑓 ↑ 𝐺) ∘𝑓
·
(𝑤
∘𝑓 ↑ 𝐺))) |
269 | 268 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘𝑓
↑
𝐺)
∘𝑓 · (𝑤 ∘𝑓 ↑ 𝐺)))) |
270 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd) |
271 | 20, 52, 31, 53, 270, 231, 239, 244 | psrbagev1 19331 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆))) |
272 | 271 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶) |
273 | 20, 52, 31, 53, 270, 235, 239, 244 | psrbagev1 19331 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆))) |
274 | 273 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶) |
275 | 271 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆)) |
276 | 273 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘𝑓 ↑ 𝐺) finSupp
(1r‘𝑆)) |
277 | 52, 53, 227, 270, 244, 272, 274, 275, 276 | gsumadd 18146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘𝑓
↑
𝐺)
∘𝑓 · (𝑤 ∘𝑓 ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
278 | 269, 277 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
279 | 278 | adantrl 748 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
280 | 229, 279 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
281 | 60 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd) |
282 | 69 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:𝐾⟶𝐶) |
283 | 282, 219 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶) |
284 | 282, 223 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) |
285 | 20, 52, 31, 53, 270, 231, 239, 244 | psrbagev2 19332 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
286 | 285 | adantrl 748 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
287 | 20, 52, 31, 53, 270, 235, 239, 244 | psrbagev2 19332 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
288 | 287 | adantrl 748 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
289 | 52, 227 | cmn4 18035 |
. . . . . . 7
⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
290 | 281, 283,
284, 286, 288, 289 | syl122anc 1327 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
291 | 280, 290 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
292 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ V) |
293 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing) |
294 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing) |
295 | 36 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
296 | 38 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶) |
297 | 20 | psrbagaddcl 19191 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘𝑓 + 𝑤) ∈ 𝐷) |
298 | 292, 218,
222, 297 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘𝑓 + 𝑤) ∈ 𝐷) |
299 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring) |
300 | 22, 225 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ 𝐾 ∧ (𝑦‘𝑤) ∈ 𝐾) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ 𝐾) |
301 | 299, 219,
223, 300 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ 𝐾) |
302 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 292, 293, 294, 295, 296, 21, 298, 301 | evlslem3 19335 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘𝑓 + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘𝑓 +
𝑤)
∘𝑓 ↑ 𝐺)))) |
303 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 292, 293, 294, 295, 296, 21, 218, 219 | evlslem3 19335 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) = ((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺)))) |
304 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 292, 293, 294, 295, 296, 21, 222, 223 | evlslem3 19335 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺)))) |
305 | 303, 304 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘𝑓
↑
𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘𝑓
↑
𝐺))))) |
306 | 291, 302,
305 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘𝑓 + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))))) |
307 | 10, 1, 5, 21, 20, 6, 7, 13, 211, 306 | evlslem2 19333 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦))) |
308 | 1, 2, 3, 4, 5, 12,
15, 93, 307, 29, 94, 95, 117, 210 | isrhmd 18552 |
. 2
⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆)) |
309 | | ovex 6577 |
. . . . . 6
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
310 | 309, 33 | fnmpti 5935 |
. . . . 5
⊢ 𝐸 Fn 𝐵 |
311 | 310 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 Fn 𝐵) |
312 | 22, 1 | rhmf 18549 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:𝐾⟶𝐵) |
313 | 87, 312 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴:𝐾⟶𝐵) |
314 | 313 | ffnd 5959 |
. . . 4
⊢ (𝜑 → 𝐴 Fn 𝐾) |
315 | | frn 5966 |
. . . . 5
⊢ (𝐴:𝐾⟶𝐵 → ran 𝐴 ⊆ 𝐵) |
316 | 313, 315 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐴 ⊆ 𝐵) |
317 | | fnco 5913 |
. . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn 𝐾 ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn 𝐾) |
318 | 311, 314,
316, 317 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn 𝐾) |
319 | 69 | ffnd 5959 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐾) |
320 | | fvco2 6183 |
. . . . 5
⊢ ((𝐴 Fn 𝐾 ∧ 𝑥 ∈ 𝐾) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) |
321 | 314, 320 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) |
322 | 321, 74 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
323 | 318, 319,
322 | eqfnfvd 6222 |
. 2
⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹) |
324 | 10, 32, 1, 6, 9 | mvrf2 19313 |
. . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) |
325 | 324 | ffnd 5959 |
. . . 4
⊢ (𝜑 → 𝑉 Fn 𝐼) |
326 | | frn 5966 |
. . . . 5
⊢ (𝑉:𝐼⟶𝐵 → ran 𝑉 ⊆ 𝐵) |
327 | 324, 326 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑉 ⊆ 𝐵) |
328 | | fnco 5913 |
. . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼) |
329 | 311, 325,
327, 328 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼) |
330 | | fvco2 6183 |
. . . . 5
⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) |
331 | 325, 330 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) |
332 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ V) |
333 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) |
334 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
335 | 32, 20, 21, 76, 332, 333, 334 | mvrval 19242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) |
336 | 335 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))) |
337 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing) |
338 | 36 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
339 | 38 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶) |
340 | 20 | psrbagsn 19316 |
. . . . . . . 8
⊢ (𝐼 ∈ V → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
341 | 6, 340 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
342 | 341 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
343 | 78 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ 𝐾) |
344 | 10, 1, 29, 22, 20, 30, 31, 5, 32, 33, 332, 333, 337, 338, 339, 21, 342, 343 | evlslem3 19335 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺)))) |
345 | 92 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
346 | | 1nn0 11185 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
347 | | 0nn0 11184 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
348 | 346, 347 | keepel 4105 |
. . . . . . . . . . . . 13
⊢ if(𝑧 = 𝑥, 1, 0) ∈
ℕ0 |
349 | 348 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈
ℕ0) |
350 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) |
351 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) |
352 | 38 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧))) |
353 | 6, 349, 350, 351, 352 | offval2 6812 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))) |
354 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) |
355 | 354 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
356 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) |
357 | 356 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
358 | 350 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶) |
359 | 52, 31 | mulg1 17371 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) |
360 | 358, 359 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) |
361 | | iftrue 4042 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) |
362 | 361 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) |
363 | 360, 362 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
364 | 52, 53, 31 | mulg0 17369 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
365 | 350, 364 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
366 | 365 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
367 | | iffalse 4045 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
368 | 367 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
369 | 366, 368 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
370 | 355, 357,
363, 369 | ifbothda 4073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
371 | 370 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
372 | 353, 371 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
373 | 372 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
374 | 373 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))) |
375 | 62 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd) |
376 | 350 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) |
377 | 29, 3 | ringidcl 18391 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝐶) |
378 | 15, 377 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶) |
379 | 378 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶) |
380 | 376, 379 | ifcld 4081 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶) |
381 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
382 | 380, 381 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶) |
383 | | eldifn 3695 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 ∈ {𝑥}) |
384 | | velsn 4141 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥) |
385 | 383, 384 | sylnib 317 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥) |
386 | 385, 367 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
387 | 386 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
388 | 387, 332 | suppss2 7216 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥}) |
389 | 52, 53, 375, 332, 334, 382, 388 | gsumpt 18184 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥)) |
390 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥)) |
391 | 361, 390 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥)) |
392 | 391, 381,
45 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) |
393 | 392 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) |
394 | 374, 389,
393 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺)) = (𝐺‘𝑥)) |
395 | 345, 394 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺))) =
((1r‘𝑆)
·
(𝐺‘𝑥))) |
396 | 29, 5, 3 | ringlidm 18394 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) |
397 | 15, 51, 396 | syl2an2r 872 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) |
398 | 395, 397 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 ↑ 𝐺))) = (𝐺‘𝑥)) |
399 | 336, 344,
398 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥)) |
400 | 331, 399 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥)) |
401 | 329, 262,
400 | eqfnfvd 6222 |
. 2
⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺) |
402 | 308, 323,
401 | 3jca 1235 |
1
⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺)) |