Step |
Hyp |
Ref |
Expression |
1 |
|
evlslem3.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
2 |
|
evlslem3.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
3 |
|
evlslem3.c |
⊢ 𝐶 = ( Base ‘ 𝑆 ) |
4 |
|
evlslem3.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
5 |
|
evlslem3.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
6 |
|
evlslem3.t |
⊢ 𝑇 = ( mulGrp ‘ 𝑆 ) |
7 |
|
evlslem3.x |
⊢ ↑ = ( .g ‘ 𝑇 ) |
8 |
|
evlslem3.m |
⊢ · = ( .r ‘ 𝑆 ) |
9 |
|
evlslem3.v |
⊢ 𝑉 = ( 𝐼 mVar 𝑅 ) |
10 |
|
evlslem3.e |
⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) |
11 |
|
evlslem3.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
12 |
|
evlslem3.r |
⊢ ( 𝜑 → 𝑅 ∈ CRing ) |
13 |
|
evlslem3.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
14 |
|
evlslem3.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) |
15 |
|
evlslem3.g |
⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 ) |
16 |
|
evlslem3.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
17 |
|
evlslem3.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝐷 ) |
18 |
|
evlslem3.q |
⊢ ( 𝜑 → 𝐻 ∈ 𝐾 ) |
19 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
20 |
12 19
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
21 |
1 5 16 4 11 20 2 18 17
|
mplmon2cl |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐵 ) |
22 |
|
fveq1 |
⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝑝 ‘ 𝑏 ) = ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) |
23 |
22
|
fveq2d |
⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) = ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) ) |
24 |
23
|
oveq1d |
⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) |
25 |
24
|
mpteq2dv |
⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) |
26 |
25
|
oveq2d |
⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) |
27 |
|
ovex |
⊢ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ∈ V |
28 |
26 10 27
|
fvmpt |
⊢ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐵 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) |
29 |
21 28
|
syl |
⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) |
30 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) |
31 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑏 → ( 𝑥 = 𝐴 ↔ 𝑏 = 𝐴 ) ) |
32 |
31
|
ifbid |
⊢ ( 𝑥 = 𝑏 → if ( 𝑥 = 𝐴 , 𝐻 , 0 ) = if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) |
33 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 ) |
34 |
16
|
fvexi |
⊢ 0 ∈ V |
35 |
34
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
36 |
18 35
|
ifexd |
⊢ ( 𝜑 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ∈ V ) |
37 |
36
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ∈ V ) |
38 |
30 32 33 37
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) = if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) |
39 |
38
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) = ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ) |
40 |
39
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) |
41 |
40
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) |
42 |
41
|
oveq2d |
⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) |
43 |
|
eqid |
⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) |
44 |
|
crngring |
⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring ) |
45 |
13 44
|
syl |
⊢ ( 𝜑 → 𝑆 ∈ Ring ) |
46 |
|
ringmnd |
⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Mnd ) |
47 |
45 46
|
syl |
⊢ ( 𝜑 → 𝑆 ∈ Mnd ) |
48 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
49 |
5 48
|
rabex2 |
⊢ 𝐷 ∈ V |
50 |
49
|
a1i |
⊢ ( 𝜑 → 𝐷 ∈ V ) |
51 |
45
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring ) |
52 |
4 3
|
rhmf |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝐾 ⟶ 𝐶 ) |
53 |
14 52
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝐾 ⟶ 𝐶 ) |
54 |
4 16
|
ring0cl |
⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 ) |
55 |
20 54
|
syl |
⊢ ( 𝜑 → 0 ∈ 𝐾 ) |
56 |
18 55
|
ifcld |
⊢ ( 𝜑 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ∈ 𝐾 ) |
57 |
53 56
|
ffvelcdmd |
⊢ ( 𝜑 → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 ) |
58 |
57
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 ) |
59 |
6 3
|
mgpbas |
⊢ 𝐶 = ( Base ‘ 𝑇 ) |
60 |
|
eqid |
⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 ) |
61 |
6
|
crngmgp |
⊢ ( 𝑆 ∈ CRing → 𝑇 ∈ CMnd ) |
62 |
13 61
|
syl |
⊢ ( 𝜑 → 𝑇 ∈ CMnd ) |
63 |
62
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑇 ∈ CMnd ) |
64 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 ) |
65 |
|
cmnmnd |
⊢ ( 𝑇 ∈ CMnd → 𝑇 ∈ Mnd ) |
66 |
62 65
|
syl |
⊢ ( 𝜑 → 𝑇 ∈ Mnd ) |
67 |
66
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑇 ∈ Mnd ) |
68 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑦 ∈ ℕ0 ) |
69 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑧 ∈ 𝐶 ) |
70 |
59 7 67 68 69
|
mulgnn0cld |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 ↑ 𝑧 ) ∈ 𝐶 ) |
71 |
5
|
psrbagf |
⊢ ( 𝑏 ∈ 𝐷 → 𝑏 : 𝐼 ⟶ ℕ0 ) |
72 |
71
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 : 𝐼 ⟶ ℕ0 ) |
73 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐺 : 𝐼 ⟶ 𝐶 ) |
74 |
|
inidm |
⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼 |
75 |
70 72 73 64 64 74
|
off |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) : 𝐼 ⟶ 𝐶 ) |
76 |
|
ovex |
⊢ ( 𝑏 ∘f ↑ 𝐺 ) ∈ V |
77 |
76
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) ∈ V ) |
78 |
75
|
ffund |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → Fun ( 𝑏 ∘f ↑ 𝐺 ) ) |
79 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 0g ‘ 𝑇 ) ∈ V ) |
80 |
5
|
psrbag |
⊢ ( 𝐼 ∈ 𝑊 → ( 𝑏 ∈ 𝐷 ↔ ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑏 “ ℕ ) ∈ Fin ) ) ) |
81 |
11 80
|
syl |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↔ ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑏 “ ℕ ) ∈ Fin ) ) ) |
82 |
81
|
simplbda |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ◡ 𝑏 “ ℕ ) ∈ Fin ) |
83 |
72
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 Fn 𝐼 ) |
84 |
83
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝑏 Fn 𝐼 ) |
85 |
15
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn 𝐼 ) |
86 |
85
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝐺 Fn 𝐼 ) |
87 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝐼 ∈ 𝑊 ) |
88 |
|
eldifi |
⊢ ( 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) → 𝑦 ∈ 𝐼 ) |
89 |
88
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝑦 ∈ 𝐼 ) |
90 |
|
fnfvof |
⊢ ( ( ( 𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑊 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) ) |
91 |
84 86 87 89 90
|
syl22anc |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) ) |
92 |
|
ffvelcdm |
⊢ ( ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 ) |
93 |
72 88 92
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 ) |
94 |
|
elnn0 |
⊢ ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 ↔ ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ ∨ ( 𝑏 ‘ 𝑦 ) = 0 ) ) |
95 |
93 94
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ ∨ ( 𝑏 ‘ 𝑦 ) = 0 ) ) |
96 |
|
eldifn |
⊢ ( 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) → ¬ 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) ) |
97 |
96
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ¬ 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) ) |
98 |
83
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑏 Fn 𝐼 ) |
99 |
88
|
ad2antlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑦 ∈ 𝐼 ) |
100 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) |
101 |
98 99 100
|
elpreimad |
⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) ) |
102 |
97 101
|
mtand |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ¬ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) |
103 |
95 102
|
orcnd |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ‘ 𝑦 ) = 0 ) |
104 |
103
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) ) |
105 |
|
ffvelcdm |
⊢ ( ( 𝐺 : 𝐼 ⟶ 𝐶 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 ) |
106 |
73 88 105
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 ) |
107 |
59 60 7
|
mulg0 |
⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 → ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0g ‘ 𝑇 ) ) |
108 |
106 107
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0g ‘ 𝑇 ) ) |
109 |
91 104 108
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) ) |
110 |
75 109
|
suppss |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑏 ∘f ↑ 𝐺 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( ◡ 𝑏 “ ℕ ) ) |
111 |
|
suppssfifsupp |
⊢ ( ( ( ( 𝑏 ∘f ↑ 𝐺 ) ∈ V ∧ Fun ( 𝑏 ∘f ↑ 𝐺 ) ∧ ( 0g ‘ 𝑇 ) ∈ V ) ∧ ( ( ◡ 𝑏 “ ℕ ) ∈ Fin ∧ ( ( 𝑏 ∘f ↑ 𝐺 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ∘f ↑ 𝐺 ) finSupp ( 0g ‘ 𝑇 ) ) |
112 |
77 78 79 82 110 111
|
syl32anc |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) finSupp ( 0g ‘ 𝑇 ) ) |
113 |
59 60 63 64 75 112
|
gsumcl |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) |
114 |
3 8
|
ringcl |
⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 ) |
115 |
51 58 113 114
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 ) |
116 |
115
|
fmpttd |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 ) |
117 |
|
eldifsnneq |
⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → ¬ 𝑏 = 𝐴 ) |
118 |
117
|
iffalsed |
⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 0 ) |
119 |
118
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 0 ) |
120 |
119
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 𝐹 ‘ 0 ) ) |
121 |
|
rhmghm |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) |
122 |
14 121
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ) |
123 |
16 43
|
ghmid |
⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) ) |
124 |
122 123
|
syl |
⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) ) |
125 |
124
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) ) |
126 |
120 125
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 0g ‘ 𝑆 ) ) |
127 |
126
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) |
128 |
45
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → 𝑆 ∈ Ring ) |
129 |
|
eldifi |
⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → 𝑏 ∈ 𝐷 ) |
130 |
129 113
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) |
131 |
3 8 43
|
ringlz |
⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) ) |
132 |
128 130 131
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) ) |
133 |
127 132
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) ) |
134 |
133 50
|
suppss2 |
⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ { 𝐴 } ) |
135 |
3 43 47 50 17 116 134
|
gsumpt |
⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) ) |
136 |
42 135
|
eqtrd |
⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) ) |
137 |
|
iftrue |
⊢ ( 𝑏 = 𝐴 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 𝐻 ) |
138 |
137
|
fveq2d |
⊢ ( 𝑏 = 𝐴 → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 𝐹 ‘ 𝐻 ) ) |
139 |
|
oveq1 |
⊢ ( 𝑏 = 𝐴 → ( 𝑏 ∘f ↑ 𝐺 ) = ( 𝐴 ∘f ↑ 𝐺 ) ) |
140 |
139
|
oveq2d |
⊢ ( 𝑏 = 𝐴 → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) = ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) |
141 |
138 140
|
oveq12d |
⊢ ( 𝑏 = 𝐴 → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ) |
142 |
|
eqid |
⊢ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) |
143 |
|
ovex |
⊢ ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ∈ V |
144 |
141 142 143
|
fvmpt |
⊢ ( 𝐴 ∈ 𝐷 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ) |
145 |
17 144
|
syl |
⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ) |
146 |
29 136 145
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ) |