Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β π
β
DivRing) |
2 | | simpl 484 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β πΌ β Fin) |
3 | | xpfi 9317 |
. . . . 5
β’ ((πΌ β Fin β§ πΌ β Fin) β (πΌ Γ πΌ) β Fin) |
4 | 2, 2, 3 | syl2anc 585 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β (πΌ Γ πΌ) β Fin) |
5 | | eqid 2733 |
. . . . 5
β’ (π
freeLMod (πΌ Γ πΌ)) = (π
freeLMod (πΌ Γ πΌ)) |
6 | 5 | frlmdim 32696 |
. . . 4
β’ ((π
β DivRing β§ (πΌ Γ πΌ) β Fin) β (dimβ(π
freeLMod (πΌ Γ πΌ))) = (β―β(πΌ Γ πΌ))) |
7 | 1, 4, 6 | syl2anc 585 |
. . 3
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβ(π
freeLMod
(πΌ Γ πΌ))) = (β―β(πΌ Γ πΌ))) |
8 | | matdim.a |
. . . . . 6
β’ π΄ = (πΌ Mat π
) |
9 | 8, 5 | matbas 21913 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(π
freeLMod
(πΌ Γ πΌ))) = (Baseβπ΄)) |
10 | 9 | eqcomd 2739 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβπ΄) =
(Baseβ(π
freeLMod
(πΌ Γ πΌ)))) |
11 | | eqidd 2734 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβπ΄) =
(Baseβπ΄)) |
12 | | ssidd 4006 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβπ΄) β
(Baseβπ΄)) |
13 | 8, 5 | matplusg 21914 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(+gβ(π
freeLMod (πΌ Γ πΌ))) = (+gβπ΄)) |
14 | 13 | oveqdr 7437 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β (Baseβπ΄) β§ π¦ β (Baseβπ΄))) β (π₯(+gβ(π
freeLMod (πΌ Γ πΌ)))π¦) = (π₯(+gβπ΄)π¦)) |
15 | 5 | frlmlvec 21316 |
. . . . . . . . 9
β’ ((π
β DivRing β§ (πΌ Γ πΌ) β Fin) β (π
freeLMod (πΌ Γ πΌ)) β LVec) |
16 | 1, 4, 15 | syl2anc 585 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π
β DivRing) β (π
freeLMod (πΌ Γ πΌ)) β LVec) |
17 | | lveclmod 20717 |
. . . . . . . 8
β’ ((π
freeLMod (πΌ Γ πΌ)) β LVec β (π
freeLMod (πΌ Γ πΌ)) β LMod) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ ((πΌ β Fin β§ π
β DivRing) β (π
freeLMod (πΌ Γ πΌ)) β LMod) |
19 | 18 | adantr 482 |
. . . . . 6
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π
freeLMod (πΌ Γ πΌ)) β LMod) |
20 | | simprl 770 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π₯ β (Baseβ(Scalarβπ΄))) |
21 | 8, 5 | matsca 21915 |
. . . . . . . . . 10
β’ ((πΌ β Fin β§ π
β DivRing) β
(Scalarβ(π
freeLMod
(πΌ Γ πΌ))) = (Scalarβπ΄)) |
22 | 21 | fveq2d 6896 |
. . . . . . . . 9
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) = (Baseβ(Scalarβπ΄))) |
23 | 22 | eqcomd 2739 |
. . . . . . . 8
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (Baseβ(Scalarβπ΄)) =
(Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))) |
25 | 20, 24 | eleqtrd 2836 |
. . . . . 6
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π₯ β (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))) |
26 | | simprr 772 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π¦ β (Baseβπ΄)) |
27 | 10 | adantr 482 |
. . . . . . 7
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (Baseβπ΄) = (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
28 | 26, 27 | eleqtrd 2836 |
. . . . . 6
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β π¦ β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
29 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(π
freeLMod (πΌ Γ πΌ))) = (Baseβ(π
freeLMod (πΌ Γ πΌ))) |
30 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβ(π
freeLMod (πΌ Γ πΌ))) = (Scalarβ(π
freeLMod (πΌ Γ πΌ))) |
31 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π β(π
freeLMod (πΌ Γ πΌ))) = ( Β·π
β(π
freeLMod (πΌ Γ πΌ))) |
32 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) = (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) |
33 | 29, 30, 31, 32 | lmodvscl 20489 |
. . . . . 6
β’ (((π
freeLMod (πΌ Γ πΌ)) β LMod β§ π₯ β (Baseβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) β§ π¦ β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
34 | 19, 25, 28, 33 | syl3anc 1372 |
. . . . 5
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) β (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
35 | 34, 27 | eleqtrrd 2837 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) β (Baseβπ΄)) |
36 | 8, 5 | matvsca 21917 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β (
Β·π β(π
freeLMod (πΌ Γ πΌ))) = ( Β·π
βπ΄)) |
37 | 36 | oveqdr 7437 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβπ΄))) β (π₯( Β·π
β(π
freeLMod (πΌ Γ πΌ)))π¦) = (π₯( Β·π
βπ΄)π¦)) |
38 | | eqid 2733 |
. . . 4
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
39 | | eqidd 2734 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β
(Baseβ(Scalarβπ΄)) = (Baseβ(Scalarβπ΄))) |
40 | 21 | fveq2d 6896 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(+gβ(Scalarβ(π
freeLMod (πΌ Γ πΌ)))) =
(+gβ(Scalarβπ΄))) |
41 | 40 | oveqdr 7437 |
. . . 4
β’ (((πΌ β Fin β§ π
β DivRing) β§ (π₯ β
(Baseβ(Scalarβπ΄)) β§ π¦ β (Baseβ(Scalarβπ΄)))) β (π₯(+gβ(Scalarβ(π
freeLMod (πΌ Γ πΌ))))π¦) = (π₯(+gβ(Scalarβπ΄))π¦)) |
42 | | drngring 20364 |
. . . . . 6
β’ (π
β DivRing β π
β Ring) |
43 | 8 | matlmod 21931 |
. . . . . 6
β’ ((πΌ β Fin β§ π
β Ring) β π΄ β LMod) |
44 | 42, 43 | sylan2 594 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β π΄ β LMod) |
45 | 8 | matsca2 21922 |
. . . . . 6
β’ ((πΌ β Fin β§ π
β DivRing) β π
= (Scalarβπ΄)) |
46 | 45, 1 | eqeltrrd 2835 |
. . . . 5
β’ ((πΌ β Fin β§ π
β DivRing) β
(Scalarβπ΄) β
DivRing) |
47 | 38 | islvec 20715 |
. . . . 5
β’ (π΄ β LVec β (π΄ β LMod β§
(Scalarβπ΄) β
DivRing)) |
48 | 44, 46, 47 | sylanbrc 584 |
. . . 4
β’ ((πΌ β Fin β§ π
β DivRing) β π΄ β LVec) |
49 | 10, 11, 12, 14, 35, 37, 30, 38, 23, 39, 41, 16, 48 | dimpropd 32693 |
. . 3
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβ(π
freeLMod
(πΌ Γ πΌ))) = (dimβπ΄)) |
50 | | hashxp 14394 |
. . . 4
β’ ((πΌ β Fin β§ πΌ β Fin) β
(β―β(πΌ Γ
πΌ)) = ((β―βπΌ) Β· (β―βπΌ))) |
51 | 2, 2, 50 | syl2anc 585 |
. . 3
β’ ((πΌ β Fin β§ π
β DivRing) β
(β―β(πΌ Γ
πΌ)) = ((β―βπΌ) Β· (β―βπΌ))) |
52 | 7, 49, 51 | 3eqtr3d 2781 |
. 2
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβπ΄) =
((β―βπΌ) Β·
(β―βπΌ))) |
53 | | matdim.n |
. . 3
β’ π = (β―βπΌ) |
54 | 53, 53 | oveq12i 7421 |
. 2
β’ (π Β· π) = ((β―βπΌ) Β· (β―βπΌ)) |
55 | 52, 54 | eqtr4di 2791 |
1
β’ ((πΌ β Fin β§ π
β DivRing) β
(dimβπ΄) = (π Β· π)) |