Step | Hyp | Ref
| Expression |
1 | | snfi 9040 |
. . . . . 6
β’ {π΄} β Fin |
2 | | eleq1 2821 |
. . . . . 6
β’ (π = {π΄} β (π β Fin β {π΄} β Fin)) |
3 | 1, 2 | mpbiri 257 |
. . . . 5
β’ (π = {π΄} β π β Fin) |
4 | 3 | adantr 481 |
. . . 4
β’ ((π = {π΄} β§ π΄ β π) β π β Fin) |
5 | 4 | 3ad2ant2 1134 |
. . 3
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β π β Fin) |
6 | | simp1 1136 |
. . 3
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β π
β π) |
7 | | simp3 1138 |
. . 3
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β π β π΅) |
8 | | d1mat2pmat.t |
. . . 4
β’ π = (π matToPolyMat π
) |
9 | | eqid 2732 |
. . . 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 22217 |
. . 3
β’ ((π β Fin β§ π
β π β§ π β π΅) β (πβπ) = (π β π, π β π β¦ (πβ(πππ)))) |
14 | 5, 6, 7, 13 | syl3anc 1371 |
. 2
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β (πβπ) = (π β π, π β π β¦ (πβ(πππ)))) |
15 | | id 22 |
. . . . . . 7
β’ (π΄ β π β π΄ β π) |
16 | | fvexd 6903 |
. . . . . . 7
β’ (π΄ β π β (πβ(π΄ππ΄)) β V) |
17 | 15, 15, 16 | 3jca 1128 |
. . . . . 6
β’ (π΄ β π β (π΄ β π β§ π΄ β π β§ (πβ(π΄ππ΄)) β V)) |
18 | 17 | adantl 482 |
. . . . 5
β’ ((π = {π΄} β§ π΄ β π) β (π΄ β π β§ π΄ β π β§ (πβ(π΄ππ΄)) β V)) |
19 | 18 | 3ad2ant2 1134 |
. . . 4
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β (π΄ β π β§ π΄ β π β§ (πβ(π΄ππ΄)) β V)) |
20 | | eqid 2732 |
. . . . 5
β’ (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) |
21 | | fvoveq1 7428 |
. . . . 5
β’ (π = π΄ β (πβ(πππ)) = (πβ(π΄ππ))) |
22 | | oveq2 7413 |
. . . . . 6
β’ (π = π΄ β (π΄ππ) = (π΄ππ΄)) |
23 | 22 | fveq2d 6892 |
. . . . 5
β’ (π = π΄ β (πβ(π΄ππ)) = (πβ(π΄ππ΄))) |
24 | 20, 21, 23 | mposn 8085 |
. . . 4
β’ ((π΄ β π β§ π΄ β π β§ (πβ(π΄ππ΄)) β V) β (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©}) |
25 | 19, 24 | syl 17 |
. . 3
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©}) |
26 | | mpoeq12 7478 |
. . . . . . 7
β’ ((π = {π΄} β§ π = {π΄}) β (π β π, π β π β¦ (πβ(πππ))) = (π β {π΄}, π β {π΄} β¦ (πβ(πππ)))) |
27 | 26 | eqeq1d 2734 |
. . . . . 6
β’ ((π = {π΄} β§ π = {π΄}) β ((π β π, π β π β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©} β (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©})) |
28 | 27 | anidms 567 |
. . . . 5
β’ (π = {π΄} β ((π β π, π β π β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©} β (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©})) |
29 | 28 | adantr 481 |
. . . 4
β’ ((π = {π΄} β§ π΄ β π) β ((π β π, π β π β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©} β (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©})) |
30 | 29 | 3ad2ant2 1134 |
. . 3
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β ((π β π, π β π β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©} β (π β {π΄}, π β {π΄} β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©})) |
31 | 25, 30 | mpbird 256 |
. 2
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β (π β π, π β π β¦ (πβ(πππ))) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©}) |
32 | 14, 31 | eqtrd 2772 |
1
β’ ((π
β π β§ (π = {π΄} β§ π΄ β π) β§ π β π΅) β (πβπ) = {β¨β¨π΄, π΄β©, (πβ(π΄ππ΄))β©}) |