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 18381 |
. . . . 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 19321 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵) |
13 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑝‘𝑏) = ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) |
14 | 13 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏))) |
15 | 14 | oveq1d 6564 |
. . . . . 6
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
16 | 15 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
17 | 16 | oveq2d 6565 |
. . . 4
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
18 | | evlslem1.e |
. . . 4
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
19 | | ovex 6577 |
. . . 4
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) ∈
V |
20 | 17, 18, 19 | fvmpt 6191 |
. . 3
⊢ ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
21 | 12, 20 | syl 17 |
. 2
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
22 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) |
23 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) ∈ V |
24 | 3, 23 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ V) |
26 | | ifexg 4107 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ 𝐾 ∧ 0 ∈ V) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
27 | 10, 25, 26 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) |
29 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝑥 = 𝐴 ↔ 𝑏 = 𝐴)) |
30 | 29 | ifbid 4058 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → if(𝑥 = 𝐴, 𝐻, 0 ) = if(𝑏 = 𝐴, 𝐻, 0 )) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) |
32 | 30, 31 | fvmptg 6189 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝐷 ∧ if(𝑏 = 𝐴, 𝐻, 0 ) ∈ V) → ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏) = if(𝑏 = 𝐴, 𝐻, 0 )) |
33 | 22, 28, 32 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏) = if(𝑏 = 𝐴, 𝐻, 0 )) |
34 | 33 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) = (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 ))) |
35 | 34 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
36 | 35 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) |
37 | 36 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))))) |
38 | | evlslem1.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
39 | | eqid 2610 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
40 | | evlslem1.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) |
41 | | crngring 18381 |
. . . . . 6
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
42 | 40, 41 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) |
43 | | ringmnd 18379 |
. . . . 5
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Mnd) |
44 | 42, 43 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Mnd) |
45 | | ovex 6577 |
. . . . . 6
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
46 | 2, 45 | rabex2 4742 |
. . . . 5
⊢ 𝐷 ∈ V |
47 | 46 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
48 | 42 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) |
49 | | evlslem1.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
50 | 4, 38 | rhmf 18549 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶) |
51 | 49, 50 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐾⟶𝐶) |
52 | 4, 3 | ring0cl 18392 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) |
53 | 8, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝐾) |
54 | 10, 53 | ifcld 4081 |
. . . . . . . 8
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ 𝐾) |
55 | 51, 54 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) |
56 | 55 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) |
57 | | evlslem1.t |
. . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) |
58 | 57, 38 | mgpbas 18318 |
. . . . . . 7
⊢ 𝐶 = (Base‘𝑇) |
59 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑇) = (0g‘𝑇) |
60 | 57 | crngmgp 18378 |
. . . . . . . . 9
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) |
61 | 40, 60 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ CMnd) |
62 | 61 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) |
63 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V) |
64 | | cmnmnd 18031 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd) |
65 | 61, 64 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ Mnd) |
66 | 65 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑇 ∈ Mnd) |
67 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ ℕ0) |
68 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
69 | | evlslem1.x |
. . . . . . . . . 10
⊢ ↑ =
(.g‘𝑇) |
70 | 58, 69 | mulgnn0cl 17381 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑧 ∈ 𝐶) → (𝑦 ↑ 𝑧) ∈ 𝐶) |
71 | 66, 67, 68, 70 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → (𝑦 ↑ 𝑧) ∈ 𝐶) |
72 | 2 | psrbagf 19186 |
. . . . . . . . 9
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) |
73 | 5, 72 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) |
74 | | evlslem1.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
75 | 74 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) |
76 | | inidm 3784 |
. . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
77 | 71, 73, 75, 63, 63, 76 | off 6810 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶) |
78 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑏 ∘𝑓
↑
𝐺) ∈
V |
79 | 78 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺) ∈ V) |
80 | 77 | ffund 5962 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑏 ∘𝑓 ↑ 𝐺)) |
81 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝑇) ∈ V |
82 | 81 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (0g‘𝑇) ∈ V) |
83 | 2 | psrbag 19185 |
. . . . . . . . . 10
⊢ (𝐼 ∈ V → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) |
84 | 5, 83 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) |
85 | 84 | simplbda 652 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (◡𝑏 “ ℕ) ∈
Fin) |
86 | 73 | ffnd 5959 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼) |
87 | 86 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑏 Fn 𝐼) |
88 | 74 | ffnd 5959 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝐼) |
89 | 88 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐺 Fn 𝐼) |
90 | 5 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐼 ∈ V) |
91 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → 𝑦 ∈ 𝐼) |
92 | 91 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑦 ∈ 𝐼) |
93 | | fnfvof 6809 |
. . . . . . . . . . 11
⊢ (((𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼) ∧ (𝐼 ∈ V ∧ 𝑦 ∈ 𝐼)) → ((𝑏 ∘𝑓 ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) |
94 | 87, 89, 90, 92, 93 | syl22anc 1319 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘𝑓
↑
𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) |
95 | | eldifn 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) |
97 | 91 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ 𝐼) |
98 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑏‘𝑦) ∈ ℕ) |
99 | 86 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑏 Fn 𝐼) |
100 | | elpreima 6245 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 Fn 𝐼 → (𝑦 ∈ (◡𝑏 “ ℕ) ↔ (𝑦 ∈ 𝐼 ∧ (𝑏‘𝑦) ∈ ℕ))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑦 ∈ (◡𝑏 “ ℕ) ↔ (𝑦 ∈ 𝐼 ∧ (𝑏‘𝑦) ∈ ℕ))) |
102 | 97, 98, 101 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ (◡𝑏 “ ℕ)) |
103 | 96, 102 | mtand 689 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ (𝑏‘𝑦) ∈ ℕ) |
104 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝑏:𝐼⟶ℕ0 ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈
ℕ0) |
105 | 73, 91, 104 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) ∈
ℕ0) |
106 | | elnn0 11171 |
. . . . . . . . . . . . 13
⊢ ((𝑏‘𝑦) ∈ ℕ0 ↔ ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) |
107 | 105, 106 | sylib 207 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) |
108 | | orel1 396 |
. . . . . . . . . . . 12
⊢ (¬
(𝑏‘𝑦) ∈ ℕ → (((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0) → (𝑏‘𝑦) = 0)) |
109 | 103, 107,
108 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) = 0) |
110 | 109 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ↑ (𝐺‘𝑦)) = (0 ↑ (𝐺‘𝑦))) |
111 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝐼⟶𝐶 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ 𝐶) |
112 | 75, 91, 111 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝐺‘𝑦) ∈ 𝐶) |
113 | 58, 59, 69 | mulg0 17369 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑦) ∈ 𝐶 → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) |
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) |
115 | 94, 110, 114 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘𝑓
↑
𝐺)‘𝑦) = (0g‘𝑇)) |
116 | 77, 115 | suppss 7212 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑏 ∘𝑓 ↑ 𝐺) supp
(0g‘𝑇))
⊆ (◡𝑏 “ ℕ)) |
117 | | suppssfifsupp 8173 |
. . . . . . . 8
⊢ ((((𝑏 ∘𝑓
↑
𝐺) ∈ V ∧ Fun
(𝑏
∘𝑓 ↑ 𝐺) ∧ (0g‘𝑇) ∈ V) ∧ ((◡𝑏 “ ℕ) ∈ Fin ∧ ((𝑏 ∘𝑓
↑
𝐺) supp
(0g‘𝑇))
⊆ (◡𝑏 “ ℕ))) → (𝑏 ∘𝑓
↑
𝐺) finSupp
(0g‘𝑇)) |
118 | 79, 80, 82, 85, 116, 117 | syl32anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺) finSupp
(0g‘𝑇)) |
119 | 58, 59, 62, 63, 77, 118 | gsumcl 18139 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
120 | | evlslem1.m |
. . . . . . 7
⊢ · =
(.r‘𝑆) |
121 | 38, 120 | ringcl 18384 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈ 𝐶) |
122 | 48, 56, 119, 121 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) ∈ 𝐶) |
123 | | eqid 2610 |
. . . . 5
⊢ (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) |
124 | 122, 123 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))):𝐷⟶𝐶) |
125 | | eldifsni 4261 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ≠ 𝐴) |
126 | 125 | neneqd 2787 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → ¬ 𝑏 = 𝐴) |
127 | 126 | iffalsed 4047 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) |
128 | 127 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) |
129 | 128 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘ 0 )) |
130 | | rhmghm 18548 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
131 | 49, 130 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |
132 | 3, 39 | ghmid 17489 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘ 0 ) =
(0g‘𝑆)) |
133 | 131, 132 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘ 0 ) =
(0g‘𝑆)) |
134 | 133 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘ 0 ) =
(0g‘𝑆)) |
135 | 129, 134 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) =
(0g‘𝑆)) |
136 | 135 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
((0g‘𝑆)
·
(𝑇
Σg (𝑏 ∘𝑓 ↑ 𝐺)))) |
137 | 42 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → 𝑆 ∈ Ring) |
138 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ∈ 𝐷) |
139 | 138, 119 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) ∈ 𝐶) |
140 | 38, 120, 39 | ringlz 18410 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝑇 Σg
(𝑏
∘𝑓 ↑ 𝐺)) ∈ 𝐶) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
(0g‘𝑆)) |
141 | 137, 139,
140 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
(0g‘𝑆)) |
142 | 136, 141 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) =
(0g‘𝑆)) |
143 | 142, 47 | suppss2 7216 |
. . . 4
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)))) supp
(0g‘𝑆))
⊆ {𝐴}) |
144 | 38, 39, 44, 47, 11, 124, 143 | gsumpt 18184 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴)) |
145 | 37, 144 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴)) |
146 | | iftrue 4042 |
. . . . . 6
⊢ (𝑏 = 𝐴 → if(𝑏 = 𝐴, 𝐻, 0 ) = 𝐻) |
147 | 146 | fveq2d 6107 |
. . . . 5
⊢ (𝑏 = 𝐴 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘𝐻)) |
148 | | oveq1 6556 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝑏 ∘𝑓 ↑ 𝐺) = (𝐴 ∘𝑓 ↑ 𝐺)) |
149 | 148 | oveq2d 6565 |
. . . . 5
⊢ (𝑏 = 𝐴 → (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺)) = (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺))) |
150 | 147, 149 | oveq12d 6567 |
. . . 4
⊢ (𝑏 = 𝐴 → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |
151 | | ovex 6577 |
. . . 4
⊢ ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺))) ∈
V |
152 | 150, 123,
151 | fvmpt 6191 |
. . 3
⊢ (𝐴 ∈ 𝐷 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |
153 | 11, 152 | syl 17 |
. 2
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓
↑
𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |
154 | 21, 145, 153 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓
↑
𝐺)))) |