Step | Hyp | Ref
| Expression |
1 | | elmapi 8842 |
. . . . . . . 8
β’ (π» β (πΎ βm β0)
β π»:β0βΆπΎ) |
2 | 1 | ffvelcdmda 7079 |
. . . . . . 7
β’ ((π» β (πΎ βm β0)
β§ πΏ β
β0) β (π»βπΏ) β πΎ) |
3 | 2 | adantl 481 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (π»βπΏ) β πΎ) |
4 | | cayhamlem2.k |
. . . . . . . . 9
β’ πΎ = (Baseβπ
) |
5 | | cayhamlem2.a |
. . . . . . . . . . . 12
β’ π΄ = (π Mat π
) |
6 | 5 | matsca2 22272 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β CRing) β π
= (Scalarβπ΄)) |
7 | 6 | 3adant3 1129 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π
= (Scalarβπ΄)) |
8 | 7 | fveq2d 6888 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (Baseβπ
) = (Baseβ(Scalarβπ΄))) |
9 | 4, 8 | eqtr2id 2779 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (Baseβ(Scalarβπ΄)) = πΎ) |
10 | 9 | eleq2d 2813 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β ((π»βπΏ) β (Baseβ(Scalarβπ΄)) β (π»βπΏ) β πΎ)) |
11 | 10 | adantr 480 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((π»βπΏ) β (Baseβ(Scalarβπ΄)) β (π»βπΏ) β πΎ)) |
12 | 3, 11 | mpbird 257 |
. . . . 5
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (π»βπΏ) β (Baseβ(Scalarβπ΄))) |
13 | | eqid 2726 |
. . . . . 6
β’
(algScβπ΄) =
(algScβπ΄) |
14 | | eqid 2726 |
. . . . . 6
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
15 | | eqid 2726 |
. . . . . 6
β’
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβπ΄)) |
16 | | cayhamlem2.m |
. . . . . 6
β’ β = (
Β·π βπ΄) |
17 | | cayhamlem2.1 |
. . . . . 6
β’ 1 =
(1rβπ΄) |
18 | 13, 14, 15, 16, 17 | asclval 21769 |
. . . . 5
β’ ((π»βπΏ) β (Baseβ(Scalarβπ΄)) β ((algScβπ΄)β(π»βπΏ)) = ((π»βπΏ) β 1 )) |
19 | 12, 18 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((algScβπ΄)β(π»βπΏ)) = ((π»βπΏ) β 1 )) |
20 | 19 | eqcomd 2732 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((π»βπΏ) β 1 ) = ((algScβπ΄)β(π»βπΏ))) |
21 | 20 | oveq2d 7420 |
. 2
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((πΏ β π) Β· ((π»βπΏ) β 1 )) = ((πΏ β π) Β· ((algScβπ΄)β(π»βπΏ)))) |
22 | 5 | matassa 22296 |
. . . . 5
β’ ((π β Fin β§ π
β CRing) β π΄ β AssAlg) |
23 | 22 | 3adant3 1129 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π΄ β AssAlg) |
24 | 23 | adantr 480 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β π΄ β AssAlg) |
25 | | eqid 2726 |
. . . . 5
β’
(mulGrpβπ΄) =
(mulGrpβπ΄) |
26 | | cayhamlem2.b |
. . . . 5
β’ π΅ = (Baseβπ΄) |
27 | 25, 26 | mgpbas 20042 |
. . . 4
β’ π΅ =
(Baseβ(mulGrpβπ΄)) |
28 | | cayhamlem2.e |
. . . 4
β’ β =
(.gβ(mulGrpβπ΄)) |
29 | | crngring 20147 |
. . . . . . . 8
β’ (π
β CRing β π
β Ring) |
30 | 29 | anim2i 616 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing) β (π β Fin β§ π
β Ring)) |
31 | 30 | 3adant3 1129 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β Fin β§ π
β Ring)) |
32 | 5 | matring 22295 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
33 | 25 | ringmgp 20141 |
. . . . . 6
β’ (π΄ β Ring β
(mulGrpβπ΄) β
Mnd) |
34 | 31, 32, 33 | 3syl 18 |
. . . . 5
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (mulGrpβπ΄) β Mnd) |
35 | 34 | adantr 480 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (mulGrpβπ΄) β Mnd) |
36 | | simprr 770 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β πΏ β
β0) |
37 | | simpl3 1190 |
. . . 4
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β π β π΅) |
38 | 27, 28, 35, 36, 37 | mulgnn0cld 19019 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β (πΏ β π) β π΅) |
39 | | cayhamlem2.r |
. . . 4
β’ Β· =
(.rβπ΄) |
40 | 13, 14, 15, 26, 39, 16 | asclmul2 21776 |
. . 3
β’ ((π΄ β AssAlg β§ (π»βπΏ) β (Baseβ(Scalarβπ΄)) β§ (πΏ β π) β π΅) β ((πΏ β π) Β· ((algScβπ΄)β(π»βπΏ))) = ((π»βπΏ) β (πΏ β π))) |
41 | 24, 12, 38, 40 | syl3anc 1368 |
. 2
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((πΏ β π) Β· ((algScβπ΄)β(π»βπΏ))) = ((π»βπΏ) β (πΏ β π))) |
42 | 21, 41 | eqtr2d 2767 |
1
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π» β (πΎ βm β0)
β§ πΏ β
β0)) β ((π»βπΏ) β (πΏ β π)) = ((πΏ β π) Β· ((π»βπΏ) β 1 ))) |