Step | Hyp | Ref
| Expression |
1 | | evlslem1.p |
. . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | evlslem1.d |
. . . 4
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
3 | | evlslem3.z |
. . . 4
⊢ 0 =
(0g‘𝑅) |
4 | | evlslem1.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
5 | | evlslem1.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
6 | | evlslem1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
7 | | crngring 18913 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
9 | | evlslem1.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
10 | | evlslem3.q |
. . . 4
⊢ (𝜑 → 𝐻 ∈ 𝐾) |
11 | | evlslem3.k |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐷) |
12 | 1, 2, 3, 4, 5, 8, 9, 10, 11 | mplmon2cl 19861 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵) |
13 | | fveq1 6433 |
. . . . . . . 8
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑝‘𝑏) = ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) |
14 | 13 | fveq2d 6438 |
. . . . . . 7
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏))) |
15 | 14 | oveq1d 6921 |
. . . . . 6
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
16 | 15 | mpteq2dv 4969 |
. . . . 5
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
17 | 16 | oveq2d 6922 |
. . . 4
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
18 | | evlslem1.e |
. . . 4
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
19 | | ovex 6938 |
. . . 4
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
20 | 17, 18, 19 | fvmpt 6530 |
. . 3
⊢ ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
21 | 12, 20 | syl 17 |
. 2
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
22 | | eqid 2826 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) |
23 | | eqeq1 2830 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (𝑥 = 𝐴 ↔ 𝑏 = 𝐴)) |
24 | 23 | ifbid 4329 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → if(𝑥 = 𝐴, 𝐻, 0 ) = if(𝑏 = 𝐴, 𝐻, 0 )) |
25 | | simpr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
26 | 3 | fvexi 6448 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ V) |
28 | | ifexg 4354 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ 𝐾 ∧ 0 ∈ V) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
29 | 10, 27, 28 | syl2anc 581 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
30 | 29 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
31 | 22, 24, 25, 30 | fvmptd3 6551 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏) = if(𝑏 = 𝐴, 𝐻, 0 )) |
32 | 31 | fveq2d 6438 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) = (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 ))) |
33 | 32 | oveq1d 6921 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
34 | 33 | mpteq2dva 4968 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
35 | 34 | oveq2d 6922 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
36 | | evlslem1.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
37 | | eqid 2826 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
38 | | evlslem1.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) |
39 | | crngring 18913 |
. . . . . 6
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) |
41 | | ringmnd 18911 |
. . . . 5
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Mnd) |
42 | 40, 41 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Mnd) |
43 | | ovex 6938 |
. . . . . 6
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
44 | 2, 43 | rabex2 5040 |
. . . . 5
⊢ 𝐷 ∈ V |
45 | 44 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
46 | 40 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
47 | | evlslem1.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
48 | 4, 36 | rhmf 19083 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐾⟶𝐶) |
50 | 4, 3 | ring0cl 18924 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) |
51 | 8, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝐾) |
52 | 10, 51 | ifcld 4352 |
. . . . . . . 8
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ 𝐾) |
53 | 49, 52 | ffvelrnd 6610 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) |
54 | 53 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) |
55 | | evlslem1.t |
. . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) |
56 | 55, 36 | mgpbas 18850 |
. . . . . . 7
⊢ 𝐶 = (Base‘𝑇) |
57 | | eqid 2826 |
. . . . . . 7
⊢
(0g‘𝑇) = (0g‘𝑇) |
58 | 55 | crngmgp 18910 |
. . . . . . . . 9
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
59 | 38, 58 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ CMnd) |
60 | 59 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
61 | 5 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V) |
62 | | cmnmnd 18562 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd) |
63 | 59, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ Mnd) |
64 | 63 | ad2antrr 719 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑇 ∈ Mnd) |
65 | | simprl 789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ ℕ0) |
66 | | simprr 791 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
67 | | evlslem1.x |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑇) |
68 | 56, 67 | mulgnn0cl 17912 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈ 𝐶) → (𝑦 ↑ 𝑧) ∈ 𝐶) |
69 | 64, 65, 66, 68 | syl3anc 1496 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → (𝑦 ↑ 𝑧) ∈ 𝐶) |
70 | 2 | psrbagf 19727 |
. . . . . . . . 9
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) |
71 | 5, 70 | sylan 577 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) |
72 | | evlslem1.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
73 | 72 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
74 | | inidm 4048 |
. . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
75 | 69, 71, 73, 61, 61, 74 | off 7173 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶) |
76 | | ovex 6938 |
. . . . . . . . 9
⊢ (𝑏 ∘𝑓
↑
𝐺) ∈
V |
77 | 76 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺) ∈ V) |
78 | 75 | ffund 6283 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑏 ∘𝑓 ↑ 𝐺)) |
79 | | fvex 6447 |
. . . . . . . . 9
⊢
(0g‘𝑇) ∈ V |
80 | 79 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (0g‘𝑇) ∈ V) |
81 | 2 | psrbag 19726 |
. . . . . . . . . 10
⊢ (𝐼 ∈ V → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) |
82 | 5, 81 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) |
83 | 82 | simplbda 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (◡𝑏 “ ℕ) ∈
Fin) |
84 | 71 | ffnd 6280 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼) |
85 | 84 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑏 Fn 𝐼) |
86 | 72 | ffnd 6280 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝐼) |
87 | 86 | ad2antrr 719 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐺 Fn 𝐼) |
88 | 5 | ad2antrr 719 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐼 ∈ V) |
89 | | eldifi 3960 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → 𝑦 ∈ 𝐼) |
90 | 89 | adantl 475 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑦 ∈ 𝐼) |
91 | | fnfvof 7172 |
. . . . . . . . . . 11
⊢ (((𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼) ∧ (𝐼 ∈ V ∧ 𝑦 ∈ 𝐼)) → ((𝑏 ∘𝑓 ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) |
92 | 85, 87, 88, 90, 91 | syl22anc 874 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘𝑓
↑
𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) |
93 | | eldifn 3961 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) |
94 | 93 | adantl 475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) |
95 | 89 | ad2antlr 720 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ 𝐼) |
96 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑏‘𝑦) ∈ ℕ) |
97 | 84 | ad2antrr 719 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑏 Fn 𝐼) |
98 | | elpreima 6587 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 Fn 𝐼 → (𝑦 ∈ (◡𝑏 “ ℕ) ↔ (𝑦 ∈ 𝐼 ∧ (𝑏‘𝑦) ∈ ℕ))) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑦 ∈ (◡𝑏 “ ℕ) ↔ (𝑦 ∈ 𝐼 ∧ (𝑏‘𝑦) ∈ ℕ))) |
100 | 95, 96, 99 | mpbir2and 706 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ (◡𝑏 “ ℕ)) |
101 | 94, 100 | mtand 852 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ (𝑏‘𝑦) ∈ ℕ) |
102 | | ffvelrn 6607 |
. . . . . . . . . . . . . 14
⊢ ((𝑏:𝐼⟶ℕ0 ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈
ℕ0) |
103 | 71, 89, 102 | syl2an 591 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) ∈
ℕ0) |
104 | | elnn0 11621 |
. . . . . . . . . . . . 13
⊢ ((𝑏‘𝑦) ∈ ℕ0 ↔ ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) |
105 | 103, 104 | sylib 210 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) |
106 | | orel1 919 |
. . . . . . . . . . . 12
⊢ (¬
(𝑏‘𝑦) ∈ ℕ → (((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0) → (𝑏‘𝑦) = 0)) |
107 | 101, 105,
106 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) = 0) |
108 | 107 | oveq1d 6921 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ↑ (𝐺‘𝑦)) = (0 ↑ (𝐺‘𝑦))) |
109 | | ffvelrn 6607 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝐼⟶𝐶 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ 𝐶) |
110 | 73, 89, 109 | syl2an 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝐺‘𝑦) ∈ 𝐶) |
111 | 56, 57, 67 | mulg0 17901 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑦) ∈ 𝐶 → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) |
113 | 92, 108, 112 | 3eqtrd 2866 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘𝑓
↑
𝐺)‘𝑦) = (0g‘𝑇)) |
114 | 75, 113 | suppss 7591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑏 ∘𝑓 ↑ 𝐺) supp
(0g‘𝑇))
⊆ (◡𝑏 “ ℕ)) |
115 | | suppssfifsupp 8560 |
. . . . . . . 8
⊢ ((((𝑏 ∘𝑓
↑
𝐺) ∈ V ∧ Fun
(𝑏
∘𝑓 ↑ 𝐺) ∧ (0g‘𝑇) ∈ V) ∧ ((◡𝑏 “ ℕ) ∈ Fin ∧ ((𝑏 ∘𝑓
↑
𝐺) supp
(0g‘𝑇))
⊆ (◡𝑏 “ ℕ))) → (𝑏 ∘𝑓
↑
𝐺) finSupp
(0g‘𝑇)) |
116 | 77, 78, 80, 83, 114, 115 | syl32anc 1503 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺) finSupp
(0g‘𝑇)) |
117 | 56, 57, 60, 61, 75, 116 | gsumcl 18670 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
118 | | evlslem1.m |
. . . . . . 7
⊢ · =
(.r‘𝑆) |
119 | 36, 118 | ringcl 18916 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈ 𝐶) |
120 | 46, 54, 117, 119 | syl3anc 1496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈ 𝐶) |
121 | 120 | fmpttd 6635 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
122 | | eldifsni 4541 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ≠ 𝐴) |
123 | 122 | neneqd 3005 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → ¬ 𝑏 = 𝐴) |
124 | 123 | iffalsed 4318 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) |
125 | 124 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) |
126 | 125 | fveq2d 6438 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘ 0 )) |
127 | | rhmghm 19082 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
128 | 47, 127 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
129 | 3, 37 | ghmid 18018 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘ 0 ) =
(0g‘𝑆)) |
130 | 128, 129 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘ 0 ) =
(0g‘𝑆)) |
131 | 130 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘ 0 ) =
(0g‘𝑆)) |
132 | 126, 131 | eqtrd 2862 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) =
(0g‘𝑆)) |
133 | 132 | oveq1d 6921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
((0g‘𝑆)
·
(𝑇
Σg (𝑏 ∘𝑓 ↑ 𝐺)))) |
134 | 40 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → 𝑆 ∈ Ring) |
135 | | eldifi 3960 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ∈ 𝐷) |
136 | 135, 117 | sylan2 588 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
137 | 36, 118, 37 | ringlz 18942 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝑇 Σg
(𝑏
∘𝑓 ↑ 𝐺)) ∈ 𝐶) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
(0g‘𝑆)) |
138 | 134, 136,
137 | syl2anc 581 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
(0g‘𝑆)) |
139 | 133, 138 | eqtrd 2862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
(0g‘𝑆)) |
140 | 139, 45 | suppss2 7595 |
. . . 4
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) supp
(0g‘𝑆))
⊆ {𝐴}) |
141 | 36, 37, 42, 45, 11, 121, 140 | gsumpt 18715 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴)) |
142 | 35, 141 | eqtrd 2862 |
. 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴)) |
143 | | iftrue 4313 |
. . . . . 6
⊢ (𝑏 = 𝐴 → if(𝑏 = 𝐴, 𝐻, 0 ) = 𝐻) |
144 | 143 | fveq2d 6438 |
. . . . 5
⊢ (𝑏 = 𝐴 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘𝐻)) |
145 | | oveq1 6913 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝑏 ∘𝑓 ↑ 𝐺) = (𝐴 ∘𝑓 ↑ 𝐺)) |
146 | 145 | oveq2d 6922 |
. . . . 5
⊢ (𝑏 = 𝐴 → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) = (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺))) |
147 | 144, 146 | oveq12d 6924 |
. . . 4
⊢ (𝑏 = 𝐴 → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |
148 | | eqid 2826 |
. . . 4
⊢ (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
149 | | ovex 6938 |
. . . 4
⊢ ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺))) ∈
V |
150 | 147, 148,
149 | fvmpt 6530 |
. . 3
⊢ (𝐴 ∈ 𝐷 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |
151 | 11, 150 | syl 17 |
. 2
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |
152 | 21, 142, 151 | 3eqtrd 2866 |
1
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |