Step | Hyp | Ref
| Expression |
1 | | snfi 7923 |
. . . . . 6
⊢ {𝐴} ∈ Fin |
2 | | eleq1 2676 |
. . . . . 6
⊢ (𝑁 = {𝐴} → (𝑁 ∈ Fin ↔ {𝐴} ∈ Fin)) |
3 | 1, 2 | mpbiri 247 |
. . . . 5
⊢ (𝑁 = {𝐴} → 𝑁 ∈ Fin) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) → 𝑁 ∈ Fin) |
5 | 4 | 3ad2ant2 1076 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin) |
6 | | simp1 1054 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ 𝑉) |
7 | | simp3 1056 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
8 | | d1mat2pmat.t |
. . . 4
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
9 | | eqid 2610 |
. . . 4
⊢ (𝑁 Mat 𝑅) = (𝑁 Mat 𝑅) |
10 | | d1mat2pmat.b |
. . . 4
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
11 | | d1mat2pmat.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
12 | | d1mat2pmat.s |
. . . 4
⊢ 𝑆 = (algSc‘𝑃) |
13 | 8, 9, 10, 11, 12 | mat2pmatval 20348 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗)))) |
14 | 5, 6, 7, 13 | syl3anc 1318 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗)))) |
15 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
16 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑆‘(𝐴𝑀𝐴)) ∈ V |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑆‘(𝐴𝑀𝐴)) ∈ V) |
18 | 15, 15, 17 | 3jca 1235 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ (𝑆‘(𝐴𝑀𝐴)) ∈ V)) |
19 | 18 | adantl 481 |
. . . . 5
⊢ ((𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ (𝑆‘(𝐴𝑀𝐴)) ∈ V)) |
20 | 19 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ (𝑆‘(𝐴𝑀𝐴)) ∈ V)) |
21 | | eqid 2610 |
. . . . 5
⊢ (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) |
22 | | oveq1 6556 |
. . . . . 6
⊢ (𝑖 = 𝐴 → (𝑖𝑀𝑗) = (𝐴𝑀𝑗)) |
23 | 22 | fveq2d 6107 |
. . . . 5
⊢ (𝑖 = 𝐴 → (𝑆‘(𝑖𝑀𝑗)) = (𝑆‘(𝐴𝑀𝑗))) |
24 | | oveq2 6557 |
. . . . . 6
⊢ (𝑗 = 𝐴 → (𝐴𝑀𝑗) = (𝐴𝑀𝐴)) |
25 | 24 | fveq2d 6107 |
. . . . 5
⊢ (𝑗 = 𝐴 → (𝑆‘(𝐴𝑀𝑗)) = (𝑆‘(𝐴𝑀𝐴))) |
26 | 21, 23, 25 | mpt2sn 7155 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ (𝑆‘(𝐴𝑀𝐴)) ∈ V) → (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) |
27 | 20, 26 | syl 17 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) |
28 | | mpt2eq12 6613 |
. . . . . . 7
⊢ ((𝑁 = {𝐴} ∧ 𝑁 = {𝐴}) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗))) = (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗)))) |
29 | 28 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝑁 = {𝐴} ∧ 𝑁 = {𝐴}) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉} ↔ (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉})) |
30 | 29 | anidms 675 |
. . . . 5
⊢ (𝑁 = {𝐴} → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉} ↔ (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉})) |
31 | 30 | adantr 480 |
. . . 4
⊢ ((𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉} ↔ (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉})) |
32 | 31 | 3ad2ant2 1076 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉} ↔ (𝑖 ∈ {𝐴}, 𝑗 ∈ {𝐴} ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉})) |
33 | 27, 32 | mpbird 246 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑆‘(𝑖𝑀𝑗))) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) |
34 | 14, 33 | eqtrd 2644 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ (𝑁 = {𝐴} ∧ 𝐴 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = {〈〈𝐴, 𝐴〉, (𝑆‘(𝐴𝑀𝐴))〉}) |