Step | Hyp | Ref
| Expression |
1 | | evlslem1.b |
. . 3
⊢ 𝐵 = (Base‘𝑃) |
2 | | eqid 2726 |
. . 3
⊢
(1r‘𝑃) = (1r‘𝑃) |
3 | | eqid 2726 |
. . 3
⊢
(1r‘𝑆) = (1r‘𝑆) |
4 | | eqid 2726 |
. . 3
⊢
(.r‘𝑃) = (.r‘𝑃) |
5 | | evlslem1.m |
. . 3
⊢ · =
(.r‘𝑆) |
6 | | evlslem1.p |
. . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
7 | | evlslem1.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
8 | | evlslem1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
9 | 8 | crngringd 20225 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | 6, 7, 9 | mplringd 22028 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Ring) |
11 | | evlslem1.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) |
12 | 11 | crngringd 20225 |
. . 3
⊢ (𝜑 → 𝑆 ∈ Ring) |
13 | | 2fveq3 6898 |
. . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅)))) |
14 | | fveq2 6893 |
. . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅))) |
15 | 13, 14 | eqeq12d 2742 |
. . . . 5
⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))) |
16 | | evlslem1.d |
. . . . . . . . 9
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
17 | | eqid 2726 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
18 | | eqid 2726 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
19 | | evlslem1.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
20 | 7 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐼 ∈ 𝑊) |
21 | 9 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
22 | | simpr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
23 | 6, 16, 17, 18, 19, 20, 21, 22 | mplascl 22073 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) |
24 | 23 | fveq2d 6897 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))) |
25 | | evlslem1.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑆) |
26 | | evlslem1.t |
. . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) |
27 | | evlslem1.x |
. . . . . . . 8
⊢ ↑ =
(.g‘𝑇) |
28 | | evlslem1.v |
. . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) |
29 | | evlslem1.e |
. . . . . . . 8
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
30 | 8 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing) |
31 | 11 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing) |
32 | | evlslem1.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
33 | 32 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
34 | | evlslem1.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
35 | 34 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼⟶𝐶) |
36 | 16 | psrbag0 22071 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑊 → (𝐼 × {0}) ∈ 𝐷) |
37 | 7, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) |
38 | 37 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷) |
39 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 20, 30, 31, 33, 35, 17, 38, 22 | evlslem3 22091 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)))) |
40 | | 0zd 12616 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ) |
41 | | fvexd 6908 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V) |
42 | | fconstmpt 5736 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)) |
44 | 34 | feqmptd 6963 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥))) |
45 | 7, 40, 41, 43, 44 | offval2 7702 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥)))) |
46 | 34 | ffvelcdmda 7090 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶) |
47 | 26, 25 | mgpbas 20119 |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (Base‘𝑇) |
48 | 26, 3 | ringidval 20162 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (0g‘𝑇) |
49 | 47, 48, 27 | mulg0 19064 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) |
50 | 46, 49 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) |
51 | 50 | mpteq2dva 5245 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) |
52 | 45, 51 | eqtrd 2766 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) |
53 | 52 | oveq2d 7432 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))) |
54 | 26 | crngmgp 20220 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
55 | 11, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ CMnd) |
56 | 55 | cmnmndd 19798 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ Mnd) |
57 | 48 | gsumz 18821 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) |
58 | 56, 7, 57 | syl2anc 582 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) |
59 | 53, 58 | eqtrd 2766 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)) = (1r‘𝑆)) |
60 | 59 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)) = (1r‘𝑆)) |
61 | 60 | oveq2d 7432 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺))) = ((𝐹‘𝑥) ·
(1r‘𝑆))) |
62 | 18, 25 | rhmf 20463 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶) |
63 | 32, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶) |
64 | 63 | ffvelcdmda 7090 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ 𝐶) |
65 | 25, 5, 3 | ringridm 20245 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) |
66 | 12, 64, 65 | syl2an2r 683 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) |
67 | 61, 66 | eqtrd 2766 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺))) = (𝐹‘𝑥)) |
68 | 24, 39, 67 | 3eqtrd 2770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) |
69 | 68 | ralrimiva 3136 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) |
70 | | eqid 2726 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
71 | 18, 70 | ringidcl 20241 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
72 | 9, 71 | syl 17 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
73 | 15, 69, 72 | rspcdva 3608 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))) |
74 | 6 | mplassa 22027 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) |
75 | 7, 8, 74 | syl2anc 582 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ AssAlg) |
76 | | eqid 2726 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
77 | 19, 76 | asclrhm 21883 |
. . . . . . . 8
⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
78 | 75, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) |
79 | 6, 7, 8 | mplsca 22018 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
80 | 79 | oveq1d 7431 |
. . . . . . 7
⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) |
81 | 78, 80 | eleqtrrd 2829 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃)) |
82 | 70, 2 | rhm1 20467 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) |
83 | 81, 82 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) |
84 | 83 | fveq2d 6897 |
. . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃))) |
85 | 70, 3 | rhm1 20467 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
86 | 32, 85 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
87 | 73, 84, 86 | 3eqtr3d 2774 |
. . 3
⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆)) |
88 | | eqid 2726 |
. . . . 5
⊢
(+g‘𝑃) = (+g‘𝑃) |
89 | | eqid 2726 |
. . . . 5
⊢
(+g‘𝑆) = (+g‘𝑆) |
90 | 10 | ringgrpd 20221 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) |
91 | 12 | ringgrpd 20221 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Grp) |
92 | | eqid 2726 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
93 | | ringcmn 20257 |
. . . . . . . . 9
⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd) |
94 | 12, 93 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CMnd) |
95 | 94 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd) |
96 | | ovex 7449 |
. . . . . . . . 9
⊢
(ℕ0 ↑m 𝐼) ∈ V |
97 | 16, 96 | rabex2 5333 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
98 | 97 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V) |
99 | 7 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ 𝑊) |
100 | 8 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing) |
101 | 11 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing) |
102 | 32 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
103 | 34 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶) |
104 | | simpr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵) |
105 | 6, 1, 25, 16, 26, 27, 5, 28, 29, 99, 100, 101, 102, 103, 104 | evlslem6 22092 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆))) |
106 | 105 | simpld 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) |
107 | 105 | simprd 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆)) |
108 | 25, 92, 95, 98, 106, 107 | gsumcl 19909 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ 𝐶) |
109 | 108, 29 | fmptd 7120 |
. . . . 5
⊢ (𝜑 → 𝐸:𝐵⟶𝐶) |
110 | | eqid 2726 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝑅) = (+g‘𝑅) |
111 | | simplrl 775 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵) |
112 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵) |
113 | 6, 1, 110, 88, 111, 112 | mpladd 22014 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘f
(+g‘𝑅)𝑦)) |
114 | 113 | fveq1d 6895 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘f
(+g‘𝑅)𝑦)‘𝑏)) |
115 | | simprl 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
116 | 6, 18, 1, 16, 115 | mplelf 22003 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶(Base‘𝑅)) |
117 | 116 | ffnd 6721 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷) |
118 | 117 | adantr 479 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷) |
119 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
120 | 6, 18, 1, 16, 119 | mplelf 22003 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶(Base‘𝑅)) |
121 | 120 | ffnd 6721 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷) |
122 | 121 | adantr 479 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷) |
123 | 97 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V) |
124 | | simpr 483 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
125 | | fnfvof 7699 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘f
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
126 | 118, 122,
123, 124, 125 | syl22anc 837 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘f
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
127 | 114, 126 | eqtrd 2766 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) |
128 | 127 | fveq2d 6897 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))) |
129 | | rhmghm 20462 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
130 | 32, 129 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
131 | 130 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
132 | 116 | ffvelcdmda 7090 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ (Base‘𝑅)) |
133 | 120 | ffvelcdmda 7090 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ (Base‘𝑅)) |
134 | 18, 110, 89 | ghmlin 19211 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ (Base‘𝑅) ∧ (𝑦‘𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
135 | 131, 132,
133, 134 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
136 | 128, 135 | eqtrd 2766 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) |
137 | 136 | oveq1d 7431 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
138 | 12 | ad2antrr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
139 | 63 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶) |
140 | 139, 132 | ffvelcdmd 7091 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶) |
141 | 139, 133 | ffvelcdmd 7091 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶) |
142 | 55 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
143 | 34 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
144 | 16, 47, 27, 142, 124, 143 | psrbagev2 22088 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) |
145 | 25, 89, 5 | ringdir 20240 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
146 | 138, 140,
141, 144, 145 | syl13anc 1369 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
147 | 137, 146 | eqtrd 2766 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
148 | 147 | mpteq2dva 5245 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
149 | 97 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V) |
150 | | ovexd 7451 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V) |
151 | | ovexd 7451 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V) |
152 | | eqidd 2727 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
153 | | eqidd 2727 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
154 | 149, 150,
151, 152, 153 | offval2 7702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
155 | 148, 154 | eqtr4d 2769 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
156 | 155 | oveq2d 7432 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) |
157 | 94 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd) |
158 | 7 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
159 | 8 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing) |
160 | 11 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing) |
161 | 32 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
162 | 34 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶) |
163 | 6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 115 | evlslem6 22092 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆))) |
164 | 163 | simpld 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) |
165 | 6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 119 | evlslem6 22092 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆))) |
166 | 165 | simpld 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) |
167 | 163 | simprd 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆)) |
168 | 165 | simprd 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆)) |
169 | 25, 92, 89, 157, 149, 164, 166, 167, 168 | gsumadd 19917 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) |
170 | 156, 169 | eqtrd 2766 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) |
171 | 90 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp) |
172 | 1, 88 | grpcl 18931 |
. . . . . . . 8
⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) |
173 | 171, 115,
119, 172 | syl3anc 1368 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) |
174 | | fveq1 6892 |
. . . . . . . . . . . 12
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏)) |
175 | 174 | fveq2d 6897 |
. . . . . . . . . . 11
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏))) |
176 | 175 | oveq1d 7431 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
177 | 176 | mpteq2dv 5247 |
. . . . . . . . 9
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
178 | 177 | oveq2d 7432 |
. . . . . . . 8
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
179 | | ovex 7449 |
. . . . . . . 8
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V |
180 | 178, 29, 179 | fvmpt 7001 |
. . . . . . 7
⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
181 | 173, 180 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
182 | | fveq1 6892 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏)) |
183 | 182 | fveq2d 6897 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏))) |
184 | 183 | oveq1d 7431 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
185 | 184 | mpteq2dv 5247 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
186 | 185 | oveq2d 7432 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
187 | | ovex 7449 |
. . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V |
188 | 186, 29, 187 | fvmpt 7001 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
189 | 115, 188 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
190 | | fveq1 6892 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏)) |
191 | 190 | fveq2d 6897 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏))) |
192 | 191 | oveq1d 7431 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
193 | 192 | mpteq2dv 5247 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
194 | 193 | oveq2d 7432 |
. . . . . . . . 9
⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
195 | | ovex 7449 |
. . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V |
196 | 194, 29, 195 | fvmpt 7001 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
197 | 196 | ad2antll 727 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
198 | 189, 197 | oveq12d 7434 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) |
199 | 170, 181,
198 | 3eqtr4d 2776 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦))) |
200 | 1, 25, 88, 89, 90, 91, 109, 199 | isghmd 19215 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆)) |
201 | | eqid 2726 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
202 | 201, 26 | rhmmhm 20457 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
203 | 32, 202 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
204 | 203 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) |
205 | | simprll 777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵) |
206 | 6, 18, 1, 16, 205 | mplelf 22003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶(Base‘𝑅)) |
207 | | simprrl 779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷) |
208 | 206, 207 | ffvelcdmd 7091 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ (Base‘𝑅)) |
209 | | simprlr 778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵) |
210 | 6, 18, 1, 16, 209 | mplelf 22003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶(Base‘𝑅)) |
211 | | simprrr 780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷) |
212 | 210, 211 | ffvelcdmd 7091 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ (Base‘𝑅)) |
213 | 201, 18 | mgpbas 20119 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
214 | | eqid 2726 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
215 | 201, 214 | mgpplusg 20117 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
216 | 26, 5 | mgpplusg 20117 |
. . . . . . . . 9
⊢ · =
(+g‘𝑇) |
217 | 213, 215,
216 | mhmlin 18778 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) |
218 | 204, 208,
212, 217 | syl3anc 1368 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) |
219 | 56 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd) |
220 | | simprl 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷) |
221 | 16 | psrbagf 21911 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0) |
222 | 220, 221 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0) |
223 | 222 | ffvelcdmda 7090 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈
ℕ0) |
224 | 16 | psrbagf 21911 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝐷 → 𝑤:𝐼⟶ℕ0) |
225 | 224 | ad2antll 727 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0) |
226 | 225 | ffvelcdmda 7090 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈
ℕ0) |
227 | 34 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶) |
228 | 227 | ffvelcdmda 7090 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶) |
229 | 47, 27, 216 | mulgnn0dir 19094 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
230 | 219, 223,
226, 228, 229 | syl13anc 1369 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
231 | 230 | mpteq2dva 5245 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) |
232 | 7 | adantr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ 𝑊) |
233 | | ovexd 7451 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V) |
234 | | fvexd 6908 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V) |
235 | 222 | ffnd 6721 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼) |
236 | 225 | ffnd 6721 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼) |
237 | | inidm 4217 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
238 | | eqidd 2727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣)) |
239 | | eqidd 2727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣)) |
240 | 235, 236,
232, 232, 237, 238, 239 | offval 7691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣)))) |
241 | 34 | feqmptd 6963 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) |
242 | 241 | adantr 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) |
243 | 232, 233,
234, 240, 242 | offval2 7702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)))) |
244 | | ovexd 7451 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) |
245 | | ovexd 7451 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) |
246 | 34 | ffnd 6721 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 Fn 𝐼) |
247 | 246 | adantr 479 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼) |
248 | | eqidd 2727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣)) |
249 | 235, 247,
232, 232, 237, 238, 248 | offval 7691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣)))) |
250 | 236, 247,
232, 232, 237, 239, 248 | offval 7691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) |
251 | 232, 244,
245, 249, 250 | offval2 7702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) |
252 | 231, 243,
251 | 3eqtr4d 2776 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) |
253 | 252 | oveq2d 7432 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)))) |
254 | 55 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd) |
255 | 16, 47, 27, 48, 254, 220, 227 | psrbagev1 22086 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆))) |
256 | 255 | simpld 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶) |
257 | | simprr 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷) |
258 | 16, 47, 27, 48, 254, 257, 227 | psrbagev1 22086 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆))) |
259 | 258 | simpld 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶) |
260 | 255 | simprd 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆)) |
261 | 258 | simprd 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆)) |
262 | 47, 48, 216, 254, 232, 256, 259, 260, 261 | gsumadd 19917 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) |
263 | 253, 262 | eqtrd 2766 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) |
264 | 263 | adantrl 714 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) |
265 | 218, 264 | oveq12d 7434 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) |
266 | 55 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd) |
267 | 63 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶) |
268 | 267, 208 | ffvelcdmd 7091 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶) |
269 | 267, 212 | ffvelcdmd 7091 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) |
270 | 16, 47, 27, 254, 220, 227 | psrbagev2 22088 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶) |
271 | 270 | adantrl 714 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶) |
272 | 16, 47, 27, 254, 257, 227 | psrbagev2 22088 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶) |
273 | 272 | adantrl 714 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶) |
274 | 47, 216 | cmn4 19795 |
. . . . . . 7
⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) |
275 | 266, 268,
269, 271, 273, 274 | syl122anc 1376 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) |
276 | 265, 275 | eqtrd 2766 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) |
277 | 7 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ 𝑊) |
278 | 8 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing) |
279 | 11 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing) |
280 | 32 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
281 | 34 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶) |
282 | 16 | psrbagaddcl 21921 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘f + 𝑤) ∈ 𝐷) |
283 | 282 | ad2antll 727 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘f + 𝑤) ∈ 𝐷) |
284 | 9 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring) |
285 | 18, 214 | ringcl 20229 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) |
286 | 284, 208,
212, 285 | syl3anc 1368 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) |
287 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 283, 286 | evlslem3 22091 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)))) |
288 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 207, 208 | evlslem3 22091 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) = ((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺)))) |
289 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 211, 212 | evlslem3 22091 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) |
290 | 288, 289 | oveq12d 7434 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) |
291 | 276, 287,
290 | 3eqtr4d 2776 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))))) |
292 | 6, 1, 5, 17, 16, 7, 8, 11, 200, 291 | evlslem2 22090 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦))) |
293 | 1, 2, 3, 4, 5, 10,
12, 87, 292, 25, 88, 89, 109, 199 | isrhmd 20466 |
. 2
⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆)) |
294 | | ovex 7449 |
. . . . . 6
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V |
295 | 294, 29 | fnmpti 6696 |
. . . . 5
⊢ 𝐸 Fn 𝐵 |
296 | 295 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 Fn 𝐵) |
297 | 18, 1 | rhmf 20463 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵) |
298 | 81, 297 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶𝐵) |
299 | 298 | ffnd 6721 |
. . . 4
⊢ (𝜑 → 𝐴 Fn (Base‘𝑅)) |
300 | 298 | frnd 6728 |
. . . 4
⊢ (𝜑 → ran 𝐴 ⊆ 𝐵) |
301 | | fnco 6670 |
. . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn (Base‘𝑅) ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn (Base‘𝑅)) |
302 | 296, 299,
300, 301 | syl3anc 1368 |
. . 3
⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn (Base‘𝑅)) |
303 | 63 | ffnd 6721 |
. . 3
⊢ (𝜑 → 𝐹 Fn (Base‘𝑅)) |
304 | | fvco2 6991 |
. . . . 5
⊢ ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) |
305 | 299, 304 | sylan 578 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) |
306 | 305, 68 | eqtrd 2766 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
307 | 302, 303,
306 | eqfnfvd 7039 |
. 2
⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹) |
308 | 6, 28, 1, 7, 9 | mvrf2 21998 |
. . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) |
309 | 308 | ffnd 6721 |
. . . 4
⊢ (𝜑 → 𝑉 Fn 𝐼) |
310 | 308 | frnd 6728 |
. . . 4
⊢ (𝜑 → ran 𝑉 ⊆ 𝐵) |
311 | | fnco 6670 |
. . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼) |
312 | 296, 309,
310, 311 | syl3anc 1368 |
. . 3
⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼) |
313 | | fvco2 6991 |
. . . . 5
⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) |
314 | 309, 313 | sylan 578 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) |
315 | 7 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
316 | 8 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) |
317 | | simpr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
318 | 28, 16, 17, 70, 315, 316, 317 | mvrval 21987 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) |
319 | 318 | fveq2d 6897 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))) |
320 | 11 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing) |
321 | 32 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
322 | 34 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶) |
323 | 16 | psrbagsn 22072 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
324 | 7, 323 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
325 | 324 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) |
326 | 72 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ (Base‘𝑅)) |
327 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 315, 316, 320, 321, 322, 17, 325, 326 | evlslem3 22091 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)))) |
328 | 86 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
329 | | 1nn0 12534 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
330 | | 0nn0 12533 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
331 | 329, 330 | ifcli 4570 |
. . . . . . . . . . . . 13
⊢ if(𝑧 = 𝑥, 1, 0) ∈
ℕ0 |
332 | 331 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈
ℕ0) |
333 | 34 | ffvelcdmda 7090 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) |
334 | | eqidd 2727 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) |
335 | 34 | feqmptd 6963 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧))) |
336 | 7, 332, 333, 334, 335 | offval2 7702 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))) |
337 | | oveq1 7423 |
. . . . . . . . . . . . . 14
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) |
338 | 337 | eqeq1d 2728 |
. . . . . . . . . . . . 13
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
339 | | oveq1 7423 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) |
340 | 339 | eqeq1d 2728 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
341 | 333 | adantr 479 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶) |
342 | 47, 27 | mulg1 19071 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) |
343 | 341, 342 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) |
344 | | iftrue 4529 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) |
345 | 344 | adantl 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) |
346 | 343, 345 | eqtr4d 2769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
347 | 47, 48, 27 | mulg0 19064 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
348 | 333, 347 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
349 | 348 | adantr 479 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) |
350 | | iffalse 4532 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
351 | 350 | adantl 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
352 | 349, 351 | eqtr4d 2769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
353 | 338, 340,
346, 352 | ifbothda 4561 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
354 | 353 | mpteq2dva 5245 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
355 | 336, 354 | eqtrd 2766 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
356 | 355 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) |
357 | 356 | oveq2d 7432 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))) |
358 | 56 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd) |
359 | 333 | adantlr 713 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) |
360 | 25, 3 | ringidcl 20241 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝐶) |
361 | 12, 360 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶) |
362 | 361 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶) |
363 | 359, 362 | ifcld 4569 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶) |
364 | 363 | fmpttd 7121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶) |
365 | | eldifsnneq 4790 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥) |
366 | 365, 350 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
367 | 366 | adantl 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) |
368 | 367, 315 | suppss2 8207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥}) |
369 | 47, 48, 358, 315, 317, 364, 368 | gsumpt 19956 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥)) |
370 | | fveq2 6893 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥)) |
371 | 344, 370 | eqtrd 2766 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥)) |
372 | | eqid 2726 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) |
373 | | fvex 6906 |
. . . . . . . . . 10
⊢ (𝐺‘𝑥) ∈ V |
374 | 371, 372,
373 | fvmpt 7001 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) |
375 | 374 | adantl 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) |
376 | 357, 369,
375 | 3eqtrd 2770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝐺‘𝑥)) |
377 | 328, 376 | oveq12d 7434 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) =
((1r‘𝑆)
·
(𝐺‘𝑥))) |
378 | 25, 5, 3 | ringlidm 20244 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) |
379 | 12, 46, 378 | syl2an2r 683 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) |
380 | 377, 379 | eqtrd 2766 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = (𝐺‘𝑥)) |
381 | 319, 327,
380 | 3eqtrd 2770 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥)) |
382 | 314, 381 | eqtrd 2766 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥)) |
383 | 312, 246,
382 | eqfnfvd 7039 |
. 2
⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺) |
384 | 293, 307,
383 | 3jca 1125 |
1
⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺)) |