Step | Hyp | Ref
| Expression |
1 | | elmapi 8793 |
. . . . . . . 8
β’ (π» β (πΎ βm β0)
β π»:β0βΆπΎ) |
2 | 1 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π» β (πΎ βm β0)
β§ πΏ β
β0) β (π»βπΏ) β πΎ) |
3 | 2 | adantl 483 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (π»βπΏ) β πΎ) |
4 | | cayhamlem2.k |
. . . . . . . . 9
β’ πΎ = (Baseβπ
) |
5 | | cayhamlem2.a |
. . . . . . . . . . . 12
β’ π΄ = (π Mat π
) |
6 | 5 | matsca2 21792 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing) β π
= (Scalarβπ΄)) |
7 | 6 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π
= (Scalarβπ΄)) |
8 | 7 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (Baseβπ
) = (Baseβ(Scalarβπ΄))) |
9 | 4, 8 | eqtr2id 2786 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (Baseβ(Scalarβπ΄)) = πΎ) |
10 | 9 | eleq2d 2820 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β ((π»βπΏ) β (Baseβ(Scalarβπ΄)) β (π»βπΏ) β πΎ)) |
11 | 10 | adantr 482 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((π»βπΏ) β (Baseβ(Scalarβπ΄)) β (π»βπΏ) β πΎ)) |
12 | 3, 11 | mpbird 257 |
. . . . 5
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (π»βπΏ) β (Baseβ(Scalarβπ΄))) |
13 | | eqid 2733 |
. . . . . 6
β’
(algScβπ΄) =
(algScβπ΄) |
14 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
15 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβπ΄)) |
16 | | cayhamlem2.m |
. . . . . 6
β’ β = (
Β·π βπ΄) |
17 | | cayhamlem2.1 |
. . . . . 6
β’ 1 =
(1rβπ΄) |
18 | 13, 14, 15, 16, 17 | asclval 21306 |
. . . . 5
β’ ((π»βπΏ) β (Baseβ(Scalarβπ΄)) β ((algScβπ΄)β(π»βπΏ)) = ((π»βπΏ) β 1 )) |
19 | 12, 18 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((algScβπ΄)β(π»βπΏ)) = ((π»βπΏ) β 1 )) |
20 | 19 | eqcomd 2739 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((π»βπΏ) β 1 ) = ((algScβπ΄)β(π»βπΏ))) |
21 | 20 | oveq2d 7377 |
. 2
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((πΏ β π) Β· ((π»βπΏ) β 1 )) = ((πΏ β π) Β· ((algScβπ΄)β(π»βπΏ)))) |
22 | 5 | matassa 21816 |
. . . . 5
β’ ((π β Fin β§ π
β CRing) β π΄ β AssAlg) |
23 | 22 | 3adant3 1133 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π΄ β AssAlg) |
24 | 23 | adantr 482 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β π΄ β AssAlg) |
25 | | eqid 2733 |
. . . . 5
β’
(mulGrpβπ΄) =
(mulGrpβπ΄) |
26 | | cayhamlem2.b |
. . . . 5
β’ π΅ = (Baseβπ΄) |
27 | 25, 26 | mgpbas 19910 |
. . . 4
β’ π΅ =
(Baseβ(mulGrpβπ΄)) |
28 | | cayhamlem2.e |
. . . 4
β’ β =
(.gβ(mulGrpβπ΄)) |
29 | | crngring 19984 |
. . . . . . . 8
β’ (π
β CRing β π
β Ring) |
30 | 29 | anim2i 618 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing) β (π β Fin β§ π
β Ring)) |
31 | 30 | 3adant3 1133 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β Fin β§ π
β Ring)) |
32 | 5 | matring 21815 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
33 | 25 | ringmgp 19978 |
. . . . . 6
β’ (π΄ β Ring β
(mulGrpβπ΄) β
Mnd) |
34 | 31, 32, 33 | 3syl 18 |
. . . . 5
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (mulGrpβπ΄) β Mnd) |
35 | 34 | adantr 482 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (mulGrpβπ΄) β Mnd) |
36 | | simprr 772 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β πΏ β
β0) |
37 | | simpl3 1194 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β π β π΅) |
38 | 27, 28, 35, 36, 37 | mulgnn0cld 18905 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (πΏ β π) β π΅) |
39 | | cayhamlem2.r |
. . . 4
β’ Β· =
(.rβπ΄) |
40 | 13, 14, 15, 26, 39, 16 | asclmul2 21313 |
. . 3
β’ ((π΄ β AssAlg β§ (π»βπΏ) β (Baseβ(Scalarβπ΄)) β§ (πΏ β π) β π΅) β ((πΏ β π) Β· ((algScβπ΄)β(π»βπΏ))) = ((π»βπΏ) β (πΏ β π))) |
41 | 24, 12, 38, 40 | syl3anc 1372 |
. 2
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((πΏ β π) Β· ((algScβπ΄)β(π»βπΏ))) = ((π»βπΏ) β (πΏ β π))) |
42 | 21, 41 | eqtr2d 2774 |
1
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((π»βπΏ) β (πΏ β π)) = ((πΏ β π) Β· ((π»βπΏ) β 1 ))) |