Step | Hyp | Ref
| Expression |
1 | | evlslem3.p |
. . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | evlslem3.d |
. . . 4
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
3 | | evlslem3.z |
. . . 4
⊢ 0 =
(0g‘𝑅) |
4 | | evlslem3.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
5 | | evlslem3.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
6 | | evlslem3.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
7 | | crngring 19602 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
9 | | evlslem3.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
10 | | evlslem3.q |
. . . 4
⊢ (𝜑 → 𝐻 ∈ 𝐾) |
11 | | evlslem3.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐷) |
12 | 1, 2, 3, 4, 5, 8, 9, 10, 11 | mplmon2cl 21053 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵) |
13 | | fveq1 6735 |
. . . . . . . 8
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑝‘𝑏) = ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) |
14 | 13 | fveq2d 6740 |
. . . . . . 7
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏))) |
15 | 14 | oveq1d 7247 |
. . . . . 6
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
16 | 15 | mpteq2dv 5166 |
. . . . 5
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
17 | 16 | oveq2d 7248 |
. . . 4
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
18 | | evlslem3.e |
. . . 4
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
19 | | ovex 7265 |
. . . 4
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V |
20 | 17, 18, 19 | fvmpt 6837 |
. . 3
⊢ ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
21 | 12, 20 | syl 17 |
. 2
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
22 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) |
23 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (𝑥 = 𝐴 ↔ 𝑏 = 𝐴)) |
24 | 23 | ifbid 4477 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → if(𝑥 = 𝐴, 𝐻, 0 ) = if(𝑏 = 𝐴, 𝐻, 0 )) |
25 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
26 | 3 | fvexi 6750 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ V) |
28 | 10, 27 | ifexd 4502 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
29 | 28 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
30 | 22, 24, 25, 29 | fvmptd3 6860 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏) = if(𝑏 = 𝐴, 𝐻, 0 )) |
31 | 30 | fveq2d 6740 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) = (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 ))) |
32 | 31 | oveq1d 7247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
33 | 32 | mpteq2dva 5165 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) |
34 | 33 | oveq2d 7248 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) |
35 | | evlslem3.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
36 | | eqid 2738 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
37 | | evlslem3.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) |
38 | | crngring 19602 |
. . . . . 6
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) |
40 | | ringmnd 19600 |
. . . . 5
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Mnd) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Mnd) |
42 | | ovex 7265 |
. . . . . 6
⊢
(ℕ0 ↑m 𝐼) ∈ V |
43 | 2, 42 | rabex2 5242 |
. . . . 5
⊢ 𝐷 ∈ V |
44 | 43 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
45 | 39 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
46 | | evlslem3.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
47 | 4, 35 | rhmf 19774 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐾⟶𝐶) |
49 | 4, 3 | ring0cl 19615 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) |
50 | 8, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝐾) |
51 | 10, 50 | ifcld 4500 |
. . . . . . . 8
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ 𝐾) |
52 | 48, 51 | ffvelrnd 6924 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) |
53 | 52 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) |
54 | | evlslem3.t |
. . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) |
55 | 54, 35 | mgpbas 19538 |
. . . . . . 7
⊢ 𝐶 = (Base‘𝑇) |
56 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝑇) = (0g‘𝑇) |
57 | 54 | crngmgp 19598 |
. . . . . . . . 9
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
58 | 37, 57 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ CMnd) |
59 | 58 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
60 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ 𝑊) |
61 | | cmnmnd 19214 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd) |
62 | 58, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ Mnd) |
63 | 62 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑇 ∈ Mnd) |
64 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ ℕ0) |
65 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
66 | | evlslem3.x |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑇) |
67 | 55, 66 | mulgnn0cl 18536 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈ 𝐶) → (𝑦 ↑ 𝑧) ∈ 𝐶) |
68 | 63, 64, 65, 67 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → (𝑦 ↑ 𝑧) ∈ 𝐶) |
69 | 2 | psrbagf 20904 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝐷 → 𝑏:𝐼⟶ℕ0) |
70 | 69 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) |
71 | | evlslem3.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
72 | 71 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
73 | | inidm 4148 |
. . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
74 | 68, 70, 72, 60, 60, 73 | off 7505 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f ↑ 𝐺):𝐼⟶𝐶) |
75 | | ovex 7265 |
. . . . . . . . 9
⊢ (𝑏 ∘f ↑ 𝐺) ∈ V |
76 | 75 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f ↑ 𝐺) ∈ V) |
77 | 74 | ffund 6568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑏 ∘f ↑ 𝐺)) |
78 | | fvexd 6751 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (0g‘𝑇) ∈ V) |
79 | 2 | psrbag 20903 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑊 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) |
80 | 5, 79 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) |
81 | 80 | simplbda 503 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (◡𝑏 “ ℕ) ∈
Fin) |
82 | 70 | ffnd 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼) |
83 | 82 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑏 Fn 𝐼) |
84 | 71 | ffnd 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝐼) |
85 | 84 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐺 Fn 𝐼) |
86 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐼 ∈ 𝑊) |
87 | | eldifi 4056 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → 𝑦 ∈ 𝐼) |
88 | 87 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑦 ∈ 𝐼) |
89 | | fnfvof 7504 |
. . . . . . . . . . 11
⊢ (((𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼) ∧ (𝐼 ∈ 𝑊 ∧ 𝑦 ∈ 𝐼)) → ((𝑏 ∘f ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) |
90 | 83, 85, 86, 88, 89 | syl22anc 839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘f ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) |
91 | | ffvelrn 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝑏:𝐼⟶ℕ0 ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈
ℕ0) |
92 | 70, 87, 91 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) ∈
ℕ0) |
93 | | elnn0 12117 |
. . . . . . . . . . . . 13
⊢ ((𝑏‘𝑦) ∈ ℕ0 ↔ ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) |
94 | 92, 93 | sylib 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) |
95 | | eldifn 4057 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) |
96 | 95 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) |
97 | 82 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑏 Fn 𝐼) |
98 | 87 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ 𝐼) |
99 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑏‘𝑦) ∈ ℕ) |
100 | 97, 98, 99 | elpreimad 6898 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ (◡𝑏 “ ℕ)) |
101 | 96, 100 | mtand 816 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ (𝑏‘𝑦) ∈ ℕ) |
102 | 94, 101 | orcnd 879 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) = 0) |
103 | 102 | oveq1d 7247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ↑ (𝐺‘𝑦)) = (0 ↑ (𝐺‘𝑦))) |
104 | | ffvelrn 6921 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝐼⟶𝐶 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ 𝐶) |
105 | 72, 87, 104 | syl2an 599 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝐺‘𝑦) ∈ 𝐶) |
106 | 55, 56, 66 | mulg0 18523 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑦) ∈ 𝐶 → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) |
107 | 105, 106 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) |
108 | 90, 103, 107 | 3eqtrd 2782 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘f ↑ 𝐺)‘𝑦) = (0g‘𝑇)) |
109 | 74, 108 | suppss 7957 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑏 ∘f ↑ 𝐺) supp (0g‘𝑇)) ⊆ (◡𝑏 “ ℕ)) |
110 | | suppssfifsupp 9025 |
. . . . . . . 8
⊢ ((((𝑏 ∘f ↑ 𝐺) ∈ V ∧ Fun (𝑏 ∘f ↑ 𝐺) ∧
(0g‘𝑇)
∈ V) ∧ ((◡𝑏 “ ℕ) ∈ Fin ∧ ((𝑏 ∘f ↑ 𝐺) supp
(0g‘𝑇))
⊆ (◡𝑏 “ ℕ))) → (𝑏 ∘f ↑ 𝐺) finSupp
(0g‘𝑇)) |
111 | 76, 77, 78, 81, 109, 110 | syl32anc 1380 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f ↑ 𝐺) finSupp (0g‘𝑇)) |
112 | 55, 56, 59, 60, 74, 111 | gsumcl 19328 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) |
113 | | evlslem3.m |
. . . . . . 7
⊢ · =
(.r‘𝑆) |
114 | 35, 113 | ringcl 19607 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ 𝐶) |
115 | 45, 53, 112, 114 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ 𝐶) |
116 | 115 | fmpttd 6951 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) |
117 | | eldifsnneq 4719 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → ¬ 𝑏 = 𝐴) |
118 | 117 | iffalsed 4465 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) |
119 | 118 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) |
120 | 119 | fveq2d 6740 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘ 0 )) |
121 | | rhmghm 19773 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
122 | 46, 121 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
123 | 3, 36 | ghmid 18656 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘ 0 ) =
(0g‘𝑆)) |
124 | 122, 123 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘ 0 ) =
(0g‘𝑆)) |
125 | 124 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘ 0 ) =
(0g‘𝑆)) |
126 | 120, 125 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) =
(0g‘𝑆)) |
127 | 126 | oveq1d 7247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) =
((0g‘𝑆)
·
(𝑇
Σg (𝑏 ∘f ↑ 𝐺)))) |
128 | 39 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → 𝑆 ∈ Ring) |
129 | | eldifi 4056 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ∈ 𝐷) |
130 | 129, 112 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) |
131 | 35, 113, 36 | ringlz 19633 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝑇 Σg
(𝑏 ∘f
↑
𝐺)) ∈ 𝐶) →
((0g‘𝑆)
·
(𝑇
Σg (𝑏 ∘f ↑ 𝐺))) = (0g‘𝑆)) |
132 | 128, 130,
131 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (0g‘𝑆)) |
133 | 127, 132 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (0g‘𝑆)) |
134 | 133, 44 | suppss2 7963 |
. . . 4
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) supp
(0g‘𝑆))
⊆ {𝐴}) |
135 | 35, 36, 41, 44, 11, 116, 134 | gsumpt 19375 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴)) |
136 | 34, 135 | eqtrd 2778 |
. 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴)) |
137 | | iftrue 4460 |
. . . . . 6
⊢ (𝑏 = 𝐴 → if(𝑏 = 𝐴, 𝐻, 0 ) = 𝐻) |
138 | 137 | fveq2d 6740 |
. . . . 5
⊢ (𝑏 = 𝐴 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘𝐻)) |
139 | | oveq1 7239 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝑏 ∘f ↑ 𝐺) = (𝐴 ∘f ↑ 𝐺)) |
140 | 139 | oveq2d 7248 |
. . . . 5
⊢ (𝑏 = 𝐴 → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) = (𝑇 Σg (𝐴 ∘f ↑ 𝐺))) |
141 | 138, 140 | oveq12d 7250 |
. . . 4
⊢ (𝑏 = 𝐴 → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) |
142 | | eqid 2738 |
. . . 4
⊢ (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) |
143 | | ovex 7265 |
. . . 4
⊢ ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺))) ∈ V |
144 | 141, 142,
143 | fvmpt 6837 |
. . 3
⊢ (𝐴 ∈ 𝐷 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) |
145 | 11, 144 | syl 17 |
. 2
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) |
146 | 21, 136, 145 | 3eqtrd 2782 |
1
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) |