Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π β Fin) |
2 | | simpr 486 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π
β Ring) |
3 | | mat2pmatbas.a |
. . . . . . . 8
β’ π΄ = (π Mat π
) |
4 | 3 | matring 21808 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
5 | | mat2pmatbas.b |
. . . . . . . 8
β’ π΅ = (Baseβπ΄) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπ΄) = (1rβπ΄) |
7 | 5, 6 | ringidcl 19994 |
. . . . . . 7
β’ (π΄ β Ring β
(1rβπ΄)
β π΅) |
8 | 4, 7 | syl 17 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β
(1rβπ΄)
β π΅) |
9 | 1, 2, 8 | 3jca 1129 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β (π β Fin β§ π
β Ring β§
(1rβπ΄)
β π΅)) |
10 | | mat2pmatbas.t |
. . . . . 6
β’ π = (π matToPolyMat π
) |
11 | | mat2pmatbas.p |
. . . . . 6
β’ π = (Poly1βπ
) |
12 | | eqid 2733 |
. . . . . 6
β’
(algScβπ) =
(algScβπ) |
13 | 10, 3, 5, 11, 12 | mat2pmatvalel 22090 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§
(1rβπ΄)
β π΅) β§ (π β π β§ π β π)) β (π(πβ(1rβπ΄))π) = ((algScβπ)β(π(1rβπ΄)π))) |
14 | 9, 13 | sylan 581 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (π(πβ(1rβπ΄))π) = ((algScβπ)β(π(1rβπ΄)π))) |
15 | | fvif 6859 |
. . . . . 6
β’
((algScβπ)βif(π = π, (1rβπ
), (0gβπ
))) = if(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))) |
16 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ
) = (1rβπ
) |
17 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ) = (1rβπ) |
18 | 11, 12, 16, 17 | ply1scl1 21679 |
. . . . . . . 8
β’ (π
β Ring β
((algScβπ)β(1rβπ
)) = (1rβπ)) |
19 | 18 | ad2antlr 726 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β ((algScβπ)β(1rβπ
)) = (1rβπ)) |
20 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
21 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
22 | 11, 12, 20, 21 | ply1scl0 21677 |
. . . . . . . 8
β’ (π
β Ring β
((algScβπ)β(0gβπ
)) = (0gβπ)) |
23 | 22 | ad2antlr 726 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β ((algScβπ)β(0gβπ
)) = (0gβπ)) |
24 | 19, 23 | ifeq12d 4508 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β if(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))) = if(π = π, (1rβπ), (0gβπ))) |
25 | 15, 24 | eqtrid 2785 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β ((algScβπ)βif(π = π, (1rβπ
), (0gβπ
))) = if(π = π, (1rβπ), (0gβπ))) |
26 | 1 | adantr 482 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β Fin) |
27 | 2 | adantr 482 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π
β Ring) |
28 | | simpl 484 |
. . . . . . . 8
β’ ((π β π β§ π β π) β π β π) |
29 | 28 | adantl 483 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β π) |
30 | | simpr 486 |
. . . . . . . 8
β’ ((π β π β§ π β π) β π β π) |
31 | 30 | adantl 483 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β π) |
32 | 3, 16, 20, 26, 27, 29, 31, 6 | mat1ov 21813 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (π(1rβπ΄)π) = if(π = π, (1rβπ
), (0gβπ
))) |
33 | 32 | fveq2d 6847 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β ((algScβπ)β(π(1rβπ΄)π)) = ((algScβπ)βif(π = π, (1rβπ
), (0gβπ
)))) |
34 | | mat2pmatbas.c |
. . . . . 6
β’ πΆ = (π Mat π) |
35 | 11 | ply1ring 21635 |
. . . . . . 7
β’ (π
β Ring β π β Ring) |
36 | 35 | ad2antlr 726 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β Ring) |
37 | | eqid 2733 |
. . . . . 6
β’
(1rβπΆ) = (1rβπΆ) |
38 | 34, 17, 21, 26, 36, 29, 31, 37 | mat1ov 21813 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (π(1rβπΆ)π) = if(π = π, (1rβπ), (0gβπ))) |
39 | 25, 33, 38 | 3eqtr4d 2783 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β ((algScβπ)β(π(1rβπ΄)π)) = (π(1rβπΆ)π)) |
40 | 14, 39 | eqtrd 2773 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (π(πβ(1rβπ΄))π) = (π(1rβπΆ)π)) |
41 | 40 | ralrimivva 3194 |
. 2
β’ ((π β Fin β§ π
β Ring) β
βπ β π βπ β π (π(πβ(1rβπ΄))π) = (π(1rβπΆ)π)) |
42 | | mat2pmatbas0.h |
. . . . 5
β’ π» = (BaseβπΆ) |
43 | 10, 3, 5, 11, 34, 42 | mat2pmatbas0 22092 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§
(1rβπ΄)
β π΅) β (πβ(1rβπ΄)) β π») |
44 | 9, 43 | syl 17 |
. . 3
β’ ((π β Fin β§ π
β Ring) β (πβ(1rβπ΄)) β π») |
45 | 11, 34 | pmatring 22057 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
46 | 42, 37 | ringidcl 19994 |
. . . 4
β’ (πΆ β Ring β
(1rβπΆ)
β π») |
47 | 45, 46 | syl 17 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
(1rβπΆ)
β π») |
48 | 34, 42 | eqmat 21789 |
. . 3
β’ (((πβ(1rβπ΄)) β π» β§ (1rβπΆ) β π») β ((πβ(1rβπ΄)) = (1rβπΆ) β βπ β π βπ β π (π(πβ(1rβπ΄))π) = (π(1rβπΆ)π))) |
49 | 44, 47, 48 | syl2anc 585 |
. 2
β’ ((π β Fin β§ π
β Ring) β ((πβ(1rβπ΄)) = (1rβπΆ) β βπ β π βπ β π (π(πβ(1rβπ΄))π) = (π(1rβπΆ)π))) |
50 | 41, 49 | mpbird 257 |
1
β’ ((π β Fin β§ π
β Ring) β (πβ(1rβπ΄)) = (1rβπΆ)) |