Step | Hyp | Ref
| Expression |
1 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝑓‘𝑛) = (𝑔‘𝑛)) |
2 | 1 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝑇‘(𝑓‘𝑛)) = (𝑇‘(𝑔‘𝑛))) |
3 | 2 | oveq2d 6565 |
. . . . . 6
⊢ (𝑓 = 𝑔 → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))) = ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))) |
4 | 3 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑓 = 𝑔 → (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))) = (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛))))) |
5 | 4 | oveq2d 6565 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) |
6 | 5 | eqeq2d 2620 |
. . 3
⊢ (𝑓 = 𝑔 → (𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛))))))) |
7 | 6 | cbvrexv 3148 |
. 2
⊢
(∃𝑓 ∈
(𝐷
↑𝑚 {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ ∃𝑔 ∈ (𝐷 ↑𝑚 {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) |
8 | | crngring 18381 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
9 | 8 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
10 | 9 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
11 | 10 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
12 | | simplr 788 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → 𝑔 ∈ (𝐷 ↑𝑚
{0})) |
13 | | simpr 476 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) |
14 | | pmatcollpw.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
15 | | pmatcollpw.c |
. . . . . . 7
⊢ 𝐶 = (𝑁 Mat 𝑃) |
16 | | pmatcollpw.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
17 | | pmatcollpw.m |
. . . . . . 7
⊢ ∗ = (
·𝑠 ‘𝐶) |
18 | | pmatcollpw.e |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
19 | | pmatcollpw.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝑅) |
20 | | pmatcollpw.t |
. . . . . . 7
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
21 | | pmatcollpw3.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
22 | | pmatcollpw3.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐴) |
23 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐴) = (0g‘𝐴) |
24 | | eqid 2610 |
. . . . . . 7
⊢ (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) |
25 | 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 | pmatcollpw3fi1lem1 20410 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) |
26 | 11, 12, 13, 25 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) |
27 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
28 | 27 | a1i 11 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) → 1 ∈
ℕ) |
29 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑠 = 1 → (0...𝑠) = (0...1)) |
30 | 29 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑠 = 1 → (𝐷 ↑𝑚 (0...𝑠)) = (𝐷 ↑𝑚
(0...1))) |
31 | 29 | mpteq1d 4666 |
. . . . . . . . . 10
⊢ (𝑠 = 1 → (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) |
32 | 31 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑠 = 1 → (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) |
33 | 32 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑠 = 1 → (𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |
34 | 30, 33 | rexeqbidv 3130 |
. . . . . . 7
⊢ (𝑠 = 1 → (∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...1))𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |
35 | 34 | adantl 481 |
. . . . . 6
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) ∧ 𝑠 = 1) → (∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...1))𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |
36 | | elmapi 7765 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝐷 ↑𝑚 {0}) →
𝑔:{0}⟶𝐷) |
37 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
V |
38 | 37 | snid 4155 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
{0} |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 ∈ (0...1) → 0 ∈
{0}) |
40 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:{0}⟶𝐷 ∧ 0 ∈ {0}) → (𝑔‘0) ∈ 𝐷) |
41 | 39, 40 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:{0}⟶𝐷 ∧ 𝑙 ∈ (0...1)) → (𝑔‘0) ∈ 𝐷) |
42 | 41 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:{0}⟶𝐷 → (𝑙 ∈ (0...1) → (𝑔‘0) ∈ 𝐷)) |
43 | 36, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝐷 ↑𝑚 {0}) →
(𝑙 ∈ (0...1) →
(𝑔‘0) ∈ 𝐷)) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) →
(𝑙 ∈ (0...1) →
(𝑔‘0) ∈ 𝐷)) |
45 | 44 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
(𝑔‘0) ∈ 𝐷) |
46 | 21 | matring 20068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
47 | 8, 46 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
48 | 47 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring) |
49 | 22, 23 | ring0cl 18392 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Ring →
(0g‘𝐴)
∈ 𝐷) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0g‘𝐴) ∈ 𝐷) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
(0g‘𝐴)
∈ 𝐷) |
52 | 45, 51 | ifcld 4081 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑙 ∈ (0...1)) →
if(𝑙 = 0, (𝑔‘0),
(0g‘𝐴))
∈ 𝐷) |
53 | 52, 24 | fmptd 6292 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) →
(𝑙 ∈ (0...1) ↦
if(𝑙 = 0, (𝑔‘0),
(0g‘𝐴))):(0...1)⟶𝐷) |
54 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐴)
∈ V |
55 | 22, 54 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈ V |
56 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (0...1)
∈ V |
57 | 55, 56 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ V ∧ (0...1) ∈
V) |
58 | | elmapg 7757 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ V ∧ (0...1) ∈
V) → ((𝑙 ∈
(0...1) ↦ if(𝑙 = 0,
(𝑔‘0),
(0g‘𝐴)))
∈ (𝐷
↑𝑚 (0...1)) ↔ (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))):(0...1)⟶𝐷)) |
59 | 57, 58 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) →
((𝑙 ∈ (0...1) ↦
if(𝑙 = 0, (𝑔‘0),
(0g‘𝐴)))
∈ (𝐷
↑𝑚 (0...1)) ↔ (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))):(0...1)⟶𝐷)) |
60 | 53, 59 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) →
(𝑙 ∈ (0...1) ↦
if(𝑙 = 0, (𝑔‘0),
(0g‘𝐴)))
∈ (𝐷
↑𝑚 (0...1))) |
61 | 60 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) ∈ (𝐷 ↑𝑚
(0...1))) |
62 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) → (𝑓‘𝑛) = ((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) → (𝑇‘(𝑓‘𝑛)) = (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛))) |
64 | 63 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) → ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))) = ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))) |
65 | 64 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) → (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))) = (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛))))) |
66 | 65 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) → (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) |
67 | 66 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴))) → (𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛))))))) |
68 | 67 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) ∧ 𝑓 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))) → (𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) ↔ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛))))))) |
69 | 61, 68 | rspcedv 3286 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → (𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛))))) → ∃𝑓 ∈ (𝐷 ↑𝑚 (0...1))𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |
70 | 69 | imp 444 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) → ∃𝑓 ∈ (𝐷 ↑𝑚 (0...1))𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) |
71 | 28, 35, 70 | rspcedvd 3289 |
. . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘((𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝑔‘0), (0g‘𝐴)))‘𝑛)))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) |
72 | 26, 71 | mpdan 699 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) ∧
𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛)))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) |
73 | 72 | ex 449 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑔 ∈ (𝐷 ↑𝑚 {0})) →
(𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |
74 | 73 | rexlimdva 3013 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑔 ∈ (𝐷 ↑𝑚 {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑔‘𝑛))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |
75 | 7, 74 | syl5bi 231 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑓 ∈ (𝐷 ↑𝑚 {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) |