Step | Hyp | Ref
| Expression |
1 | | scmatid.e |
. . . . 5
β’ πΈ = (Baseβπ
) |
2 | | scmatid.a |
. . . . 5
β’ π΄ = (π Mat π
) |
3 | | scmatid.b |
. . . . 5
β’ π΅ = (Baseβπ΄) |
4 | | eqid 2733 |
. . . . 5
β’
(1rβπ΄) = (1rβπ΄) |
5 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ΄) = ( Β·π
βπ΄) |
6 | | scmatid.s |
. . . . 5
β’ π = (π ScMat π
) |
7 | 1, 2, 3, 4, 5, 6 | scmatscmid 21878 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ π β π) β βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄))) |
8 | 7 | 3expa 1119 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ π β π) β βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄))) |
9 | 8 | adantrr 716 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄))) |
10 | 1, 2, 3, 4, 5, 6 | scmatscmid 21878 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π) β βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄))) |
11 | 10 | 3expia 1122 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β (π β π β βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)))) |
12 | | oveq12 7370 |
. . . . . . . . . . 11
β’ ((π = (π( Β·π
βπ΄)(1rβπ΄)) β§ π = (π( Β·π
βπ΄)(1rβπ΄))) β (π(-gβπ΄)π) = ((π( Β·π
βπ΄)(1rβπ΄))(-gβπ΄)(π( Β·π
βπ΄)(1rβπ΄)))) |
13 | 12 | adantl 483 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ π
β Ring) β§
π β πΈ) β§ π β πΈ) β§ (π = (π( Β·π
βπ΄)(1rβπ΄)) β§ π = (π( Β·π
βπ΄)(1rβπ΄)))) β (π(-gβπ΄)π) = ((π( Β·π
βπ΄)(1rβπ΄))(-gβπ΄)(π( Β·π
βπ΄)(1rβπ΄)))) |
14 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
15 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβπ΄)) |
16 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(-gβπ΄) = (-gβπ΄) |
17 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(-gβ(Scalarβπ΄)) =
(-gβ(Scalarβπ΄)) |
18 | 2 | matlmod 21801 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β Ring) β π΄ β LMod) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β π΄ β LMod) |
20 | 2 | matsca2 21792 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Fin β§ π
β Ring) β π
= (Scalarβπ΄)) |
21 | 20 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Fin β§ π
β Ring) β
(Baseβπ
) =
(Baseβ(Scalarβπ΄))) |
22 | 1, 21 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π
β Ring) β πΈ =
(Baseβ(Scalarβπ΄))) |
23 | 22 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β Ring) β (π β πΈ β π β (Baseβ(Scalarβπ΄)))) |
24 | 23 | biimpd 228 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π
β Ring) β (π β πΈ β π β (Baseβ(Scalarβπ΄)))) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β Fin β§ π
β Ring) β§ π β πΈ) β (π β πΈ β π β (Baseβ(Scalarβπ΄)))) |
26 | 25 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β π β (Baseβ(Scalarβπ΄))) |
27 | 22 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π
β Ring) β (π β πΈ β π β (Baseβ(Scalarβπ΄)))) |
28 | 27 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ (((π β Fin β§ π
β Ring) β§ π β πΈ) β π β (Baseβ(Scalarβπ΄))) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β π β (Baseβ(Scalarβπ΄))) |
30 | 2 | matring 21815 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
31 | 3, 4 | ringidcl 19997 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β Ring β
(1rβπ΄)
β π΅) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β Ring) β
(1rβπ΄)
β π΅) |
33 | 32 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (1rβπ΄) β π΅) |
34 | 3, 5, 14, 15, 16, 17, 19, 26, 29, 33 | lmodsubdir 20424 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = ((π( Β·π
βπ΄)(1rβπ΄))(-gβπ΄)(π( Β·π
βπ΄)(1rβπ΄)))) |
35 | 34 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β ((π( Β·π
βπ΄)(1rβπ΄))(-gβπ΄)(π( Β·π
βπ΄)(1rβπ΄))) = ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄))) |
36 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (π β Fin β§ π
β Ring)) |
37 | 20 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π
β Ring) β
(Scalarβπ΄) = π
) |
38 | 37 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (Scalarβπ΄) = π
) |
39 | 38 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β
(-gβ(Scalarβπ΄)) = (-gβπ
)) |
40 | 39 | oveqd 7378 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (π(-gβ(Scalarβπ΄))π) = (π(-gβπ
)π)) |
41 | | ringgrp 19977 |
. . . . . . . . . . . . . . . . . 18
β’ (π
β Ring β π
β Grp) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β Ring) β π
β Grp) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β π
β Grp) |
44 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β π β πΈ) |
45 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β π β πΈ) |
46 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(-gβπ
) = (-gβπ
) |
47 | 1, 46 | grpsubcl 18835 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Grp β§ π β πΈ β§ π β πΈ) β (π(-gβπ
)π) β πΈ) |
48 | 43, 44, 45, 47 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (π(-gβπ
)π) β πΈ) |
49 | 40, 48 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (π(-gβ(Scalarβπ΄))π) β πΈ) |
50 | 1, 2, 3, 5 | matvscl 21803 |
. . . . . . . . . . . . . 14
β’ (((π β Fin β§ π
β Ring) β§ ((π(-gβ(Scalarβπ΄))π) β πΈ β§ (1rβπ΄) β π΅)) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π΅) |
51 | 36, 49, 33, 50 | syl12anc 836 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π΅) |
52 | | oveq1 7368 |
. . . . . . . . . . . . . . . 16
β’ (π = (π(-gβ(Scalarβπ΄))π) β (π( Β·π
βπ΄)(1rβπ΄)) = ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄))) |
53 | 52 | eqeq2d 2744 |
. . . . . . . . . . . . . . 15
β’ (π = (π(-gβ(Scalarβπ΄))π) β (((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = (π( Β·π
βπ΄)(1rβπ΄)) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)))) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β Ring) β§
π β πΈ) β§ π β πΈ) β§ π = (π(-gβ(Scalarβπ΄))π)) β (((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = (π( Β·π
βπ΄)(1rβπ΄)) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)))) |
55 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄))) |
56 | 49, 54, 55 | rspcedvd 3585 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β βπ β πΈ ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = (π( Β·π
βπ΄)(1rβπ΄))) |
57 | 1, 2, 3, 4, 5, 6 | scmatel 21877 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β Ring) β (((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π β (((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π΅ β§ βπ β πΈ ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = (π( Β·π
βπ΄)(1rβπ΄))))) |
58 | 57 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π β (((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π΅ β§ βπ β πΈ ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) = (π( Β·π
βπ΄)(1rβπ΄))))) |
59 | 51, 56, 58 | mpbir2and 712 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β ((π(-gβ(Scalarβπ΄))π)( Β·π
βπ΄)(1rβπ΄)) β π) |
60 | 35, 59 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β ((π( Β·π
βπ΄)(1rβπ΄))(-gβπ΄)(π( Β·π
βπ΄)(1rβπ΄))) β π) |
61 | 60 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ π
β Ring) β§
π β πΈ) β§ π β πΈ) β§ (π = (π( Β·π
βπ΄)(1rβπ΄)) β§ π = (π( Β·π
βπ΄)(1rβπ΄)))) β ((π( Β·π
βπ΄)(1rβπ΄))(-gβπ΄)(π( Β·π
βπ΄)(1rβπ΄))) β π) |
62 | 13, 61 | eqeltrd 2834 |
. . . . . . . . 9
β’
(((((π β Fin
β§ π
β Ring) β§
π β πΈ) β§ π β πΈ) β§ (π = (π( Β·π
βπ΄)(1rβπ΄)) β§ π = (π( Β·π
βπ΄)(1rβπ΄)))) β (π(-gβπ΄)π) β π) |
63 | 62 | exp32 422 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ π β πΈ) β§ π β πΈ) β (π = (π( Β·π
βπ΄)(1rβπ΄)) β (π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π))) |
64 | 63 | rexlimdva 3149 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ π β πΈ) β (βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π))) |
65 | 64 | com23 86 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ π β πΈ) β (π = (π( Β·π
βπ΄)(1rβπ΄)) β (βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π))) |
66 | 65 | rexlimdva 3149 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β
(βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π))) |
67 | 11, 66 | syldc 48 |
. . . 4
β’ (π β π β ((π β Fin β§ π
β Ring) β (βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π))) |
68 | 67 | adantl 483 |
. . 3
β’ ((π β π β§ π β π) β ((π β Fin β§ π
β Ring) β (βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π))) |
69 | 68 | impcom 409 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (βπ β πΈ π = (π( Β·π
βπ΄)(1rβπ΄)) β (π(-gβπ΄)π) β π)) |
70 | 9, 69 | mpd 15 |
1
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (π(-gβπ΄)π) β π) |