Step | Hyp | Ref
| Expression |
1 | | simpr 483 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β π
β
DivRing) |
2 | | simpl 481 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β πΌ β Fin) |
3 | | xpfi 9321 |
. . . . 5
β’ ((πΌ β Fin β§ πΌ β Fin) β (πΌ Γ πΌ) β Fin) |
4 | 2, 2, 3 | syl2anc 582 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β (πΌ Γ πΌ) β Fin) |
5 | | eqid 2730 |
. . . . 5
β’ (π
freeLMod (πΌ Γ πΌ)) = (π
freeLMod (πΌ Γ πΌ)) |
6 | 5 | frlmdim 32982 |
. . . 4
β’ ((π
β DivRing β§ (πΌ Γ πΌ) β Fin) β (dimβ(π
freeLMod (πΌ Γ πΌ))) = (β―β(πΌ Γ πΌ))) |
7 | 1, 4, 6 | syl2anc 582 |
. . 3
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβ(π
freeLMod
(πΌ Γ πΌ))) = (β―β(πΌ Γ πΌ))) |
8 | | matdim.a |
. . . . . 6
β’ π΄ = (πΌ Mat π
) |
9 | 8, 5 | matbas 22135 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(π
freeLMod
(πΌ Γ πΌ))) = (Baseβπ΄)) |
10 | 9 | eqcomd 2736 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβπ΄) =
(Baseβ(π
freeLMod
(πΌ Γ πΌ)))) |
11 | | eqidd 2731 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβπ΄) =
(Baseβπ΄)) |
12 | | ssidd 4006 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβπ΄) β
(Baseβπ΄)) |
13 | 8, 5 | matplusg 22136 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(+gβ(π
freeLMod (πΌ Γ πΌ))) = (+gβπ΄)) |
14 | 13 | oveqdr 7441 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β (Baseβπ΄) β§ π¦ β (Baseβπ΄))) β (π₯(+gβ(π
freeLMod (πΌ Γ πΌ)))π¦) = (π₯(+gβπ΄)π¦)) |
15 | 5 | frlmlvec 21537 |
. . . . . . . . 9
β’ ((π
β DivRing β§ (πΌ Γ πΌ) β Fin) β (π
freeLMod (πΌ Γ πΌ)) β LVec) |
16 | 1, 4, 15 | syl2anc 582 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π
β DivRing) β (π
freeLMod (πΌ Γ πΌ)) β LVec) |
17 | | lveclmod 20863 |
. . . . . . . 8
β’ ((π
freeLMod (πΌ Γ πΌ)) β LVec β (π
freeLMod (πΌ Γ πΌ)) β LMod) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ ((πΌ β Fin β§ π
β DivRing) β (π
freeLMod (πΌ Γ πΌ)) β LMod) |
19 | 18 | adantr 479 |
. . . . . 6
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π
freeLMod (πΌ Γ πΌ)) β LMod) |
20 | | simprl 767 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π₯ β (Baseβ(Scalarβπ΄))) |
21 | 8, 5 | matsca 22137 |
. . . . . . . . . 10
β’ ((πΌ β Fin β§ π
β DivRing) β
(Scalarβ(π
freeLMod
(πΌ Γ πΌ))) = (Scalarβπ΄)) |
22 | 21 | fveq2d 6896 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) = (Baseβ(Scalarβπ΄))) |
23 | 22 | eqcomd 2736 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))) |
24 | 23 | adantr 479 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (Baseβ(Scalarβπ΄)) =
(Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))) |
25 | 20, 24 | eleqtrd 2833 |
. . . . . 6
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π₯ β (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))) |
26 | | simprr 769 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π¦ β (Baseβπ΄)) |
27 | 10 | adantr 479 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (Baseβπ΄) = (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
28 | 26, 27 | eleqtrd 2833 |
. . . . . 6
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π¦ β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
29 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(π
freeLMod (πΌ Γ πΌ))) = (Baseβ(π
freeLMod (πΌ Γ πΌ))) |
30 | | eqid 2730 |
. . . . . . 7
β’
(Scalarβ(π
freeLMod (πΌ Γ πΌ))) = (Scalarβ(π
freeLMod (πΌ Γ πΌ))) |
31 | | eqid 2730 |
. . . . . . 7
β’ (
Β·π β(π
freeLMod (πΌ Γ πΌ))) = ( Β·π
β(π
freeLMod (πΌ Γ πΌ))) |
32 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) = (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) |
33 | 29, 30, 31, 32 | lmodvscl 20634 |
. . . . . 6
β’ (((π
freeLMod (πΌ Γ πΌ)) β LMod β§ π₯ β (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) β§ π¦ β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
34 | 19, 25, 28, 33 | syl3anc 1369 |
. . . . 5
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
35 | 34, 27 | eleqtrrd 2834 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) β (Baseβπ΄)) |
36 | 8, 5 | matvsca 22139 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β (
Β·π β(π
freeLMod (πΌ Γ πΌ))) = ( Β·π
βπ΄)) |
37 | 36 | oveqdr 7441 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) = (π₯( Β·π
βπ΄)π¦)) |
38 | | eqid 2730 |
. . . 4
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
39 | | eqidd 2731 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβπ΄))) |
40 | 21 | fveq2d 6896 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(+gβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) =
(+gβ(Scalarβπ΄))) |
41 | 40 | oveqdr 7441 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβ(Scalarβπ΄)))) β (π₯(+gβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))π¦) = (π₯(+gβ(Scalarβπ΄))π¦)) |
42 | | drngring 20509 |
. . . . . 6
β’ (π
β DivRing β π
β Ring) |
43 | 8 | matlmod 22153 |
. . . . . 6
β’ ((πΌ β Fin β§ π
β Ring) β π΄ β LMod) |
44 | 42, 43 | sylan2 591 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β π΄ β LMod) |
45 | 8 | matsca2 22144 |
. . . . . 6
β’ ((πΌ β Fin β§ π
β DivRing) β π
= (Scalarβπ΄)) |
46 | 45, 1 | eqeltrrd 2832 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(Scalarβπ΄) β
DivRing) |
47 | 38 | islvec 20861 |
. . . . 5
β’ (π΄ β LVec β (π΄ β LMod β§
(Scalarβπ΄) β
DivRing)) |
48 | 44, 46, 47 | sylanbrc 581 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β π΄ β LVec) |
49 | 10, 11, 12, 14, 35, 37, 30, 38, 23, 39, 41, 16, 48 | dimpropd 32979 |
. . 3
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβ(π
freeLMod
(πΌ Γ πΌ))) = (dimβπ΄)) |
50 | | hashxp 14400 |
. . . 4
β’ ((πΌ β Fin β§ πΌ β Fin) β
(β―β(πΌ Γ
πΌ)) = ((β―βπΌ) Β· (β―βπΌ))) |
51 | 2, 2, 50 | syl2anc 582 |
. . 3
β’ ((πΌ β Fin β§ π
β DivRing) β
(β―β(πΌ Γ
πΌ)) = ((β―βπΌ) Β· (β―βπΌ))) |
52 | 7, 49, 51 | 3eqtr3d 2778 |
. 2
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβπ΄) =
((β―βπΌ) Β·
(β―βπΌ))) |
53 | | matdim.n |
. . 3
β’ π = (β―βπΌ) |
54 | 53, 53 | oveq12i 7425 |
. 2
β’ (π Β· π) = ((β―βπΌ) Β· (β―βπΌ)) |
55 | 52, 54 | eqtr4di 2788 |
1
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβπ΄) = (π Β· π)) |