| Step | Hyp | Ref
| Expression |
| 1 | | cpmat.s |
. 2
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
| 2 | | df-cpmat 22712 |
. . . 4
⊢
ConstPolyMat = (𝑛 ∈
Fin, 𝑟 ∈ V ↦
{𝑚 ∈
(Base‘(𝑛 Mat
(Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)}) |
| 3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})) |
| 4 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
| 5 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
| 6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
| 7 | 4, 6 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat (Poly1‘𝑟)) = (𝑁 Mat (Poly1‘𝑅))) |
| 8 | 7 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat (Poly1‘𝑟))) = (Base‘(𝑁 Mat
(Poly1‘𝑅)))) |
| 9 | | cpmat.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
| 10 | | cpmat.c |
. . . . . . . . 9
⊢ 𝐶 = (𝑁 Mat 𝑃) |
| 11 | | cpmat.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
| 12 | 11 | oveq2i 7442 |
. . . . . . . . 9
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat (Poly1‘𝑅)) |
| 13 | 10, 12 | eqtri 2765 |
. . . . . . . 8
⊢ 𝐶 = (𝑁 Mat (Poly1‘𝑅)) |
| 14 | 13 | fveq2i 6909 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘(𝑁 Mat
(Poly1‘𝑅))) |
| 15 | 9, 14 | eqtri 2765 |
. . . . . 6
⊢ 𝐵 = (Base‘(𝑁 Mat
(Poly1‘𝑅))) |
| 16 | 8, 15 | eqtr4di 2795 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat (Poly1‘𝑟))) = 𝐵) |
| 17 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
| 18 | 17 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (0g‘𝑟) = (0g‘𝑅)) |
| 19 | 18 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅))) |
| 20 | 19 | ralbidv 3178 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅))) |
| 21 | 4, 20 | raleqbidv 3346 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅))) |
| 22 | 4, 21 | raleqbidv 3346 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅))) |
| 23 | 16, 22 | rabeqbidv 3455 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)} = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)}) |
| 24 | 23 | adantl 481 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)} = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)}) |
| 25 | | simpl 482 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin) |
| 26 | | elex 3501 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
| 27 | 26 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V) |
| 28 | 9 | fvexi 6920 |
. . . 4
⊢ 𝐵 ∈ V |
| 29 | | rabexg 5337 |
. . . 4
⊢ (𝐵 ∈ V → {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)} ∈ V) |
| 30 | 28, 29 | mp1i 13 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)} ∈ V) |
| 31 | 3, 24, 25, 27, 30 | ovmpod 7585 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 ConstPolyMat 𝑅) = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)}) |
| 32 | 1, 31 | eqtrid 2789 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ
((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)}) |