Step | Hyp | Ref
| Expression |
1 | | drngring 20206 |
. . . . . . 7
β’ (π
β DivRing β π
β Ring) |
2 | | eqid 2737 |
. . . . . . . 8
β’ (π
freeLMod πΌ) = (π
freeLMod πΌ) |
3 | 2 | frlmlmod 21171 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β Fin) β (π
freeLMod πΌ) β LMod) |
4 | 1, 3 | sylan 581 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin) β (π
freeLMod πΌ) β LMod) |
5 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(π
freeLMod πΌ)) =
(Baseβ(π
freeLMod
πΌ)) |
6 | | eqid 2737 |
. . . . . . 7
β’
(LSubSpβ(π
freeLMod πΌ)) =
(LSubSpβ(π
freeLMod
πΌ)) |
7 | 5, 6 | lssmre 20443 |
. . . . . 6
β’ ((π
freeLMod πΌ) β LMod β (LSubSpβ(π
freeLMod πΌ)) β (Mooreβ(Baseβ(π
freeLMod πΌ)))) |
8 | 4, 7 | syl 17 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin) β
(LSubSpβ(π
freeLMod
πΌ)) β
(Mooreβ(Baseβ(π
freeLMod πΌ)))) |
9 | 8 | 3adant3 1133 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β (LSubSpβ(π
freeLMod πΌ)) β (Mooreβ(Baseβ(π
freeLMod πΌ)))) |
10 | | eqid 2737 |
. . . 4
β’
(mrClsβ(LSubSpβ(π
freeLMod πΌ))) = (mrClsβ(LSubSpβ(π
freeLMod πΌ))) |
11 | | eqid 2737 |
. . . 4
β’
(mrIndβ(LSubSpβ(π
freeLMod πΌ))) = (mrIndβ(LSubSpβ(π
freeLMod πΌ))) |
12 | 2 | frlmsca 21175 |
. . . . . . . . 9
β’ ((π
β DivRing β§ πΌ β Fin) β π
= (Scalarβ(π
freeLMod πΌ))) |
13 | | simpl 484 |
. . . . . . . . 9
β’ ((π
β DivRing β§ πΌ β Fin) β π
β
DivRing) |
14 | 12, 13 | eqeltrrd 2839 |
. . . . . . . 8
β’ ((π
β DivRing β§ πΌ β Fin) β
(Scalarβ(π
freeLMod
πΌ)) β
DivRing) |
15 | | eqid 2737 |
. . . . . . . . 9
β’
(Scalarβ(π
freeLMod πΌ)) =
(Scalarβ(π
freeLMod
πΌ)) |
16 | 15 | islvec 20581 |
. . . . . . . 8
β’ ((π
freeLMod πΌ) β LVec β ((π
freeLMod πΌ) β LMod β§ (Scalarβ(π
freeLMod πΌ)) β DivRing)) |
17 | 4, 14, 16 | sylanbrc 584 |
. . . . . . 7
β’ ((π
β DivRing β§ πΌ β Fin) β (π
freeLMod πΌ) β LVec) |
18 | 6, 10, 5 | lssacsex 20621 |
. . . . . . 7
β’ ((π
freeLMod πΌ) β LVec β ((LSubSpβ(π
freeLMod πΌ)) β (ACSβ(Baseβ(π
freeLMod πΌ))) β§ βπ₯ β π« (Baseβ(π
freeLMod πΌ))βπ¦ β (Baseβ(π
freeLMod πΌ))βπ§ β (((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π¦})) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βπ₯))π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π§})))) |
19 | 17, 18 | syl 17 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin) β
((LSubSpβ(π
freeLMod
πΌ)) β
(ACSβ(Baseβ(π
freeLMod πΌ))) β§
βπ₯ β π«
(Baseβ(π
freeLMod
πΌ))βπ¦ β (Baseβ(π
freeLMod πΌ))βπ§ β (((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π¦})) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βπ₯))π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π§})))) |
20 | 19 | simprd 497 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin) β
βπ₯ β π«
(Baseβ(π
freeLMod
πΌ))βπ¦ β (Baseβ(π
freeLMod πΌ))βπ§ β (((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π¦})) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βπ₯))π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π§}))) |
21 | 20 | 3adant3 1133 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β βπ₯ β π« (Baseβ(π
freeLMod πΌ))βπ¦ β (Baseβ(π
freeLMod πΌ))βπ§ β (((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π¦})) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βπ₯))π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π₯ βͺ {π§}))) |
22 | | dif0 4337 |
. . . . . 6
β’
((Baseβ(π
freeLMod πΌ)) β
β
) = (Baseβ(π
freeLMod πΌ)) |
23 | 22 | linds1 21232 |
. . . . 5
β’ (π β (LIndSβ(π
freeLMod πΌ)) β π β ((Baseβ(π
freeLMod πΌ)) β β
)) |
24 | 23 | 3ad2ant3 1136 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β π β ((Baseβ(π
freeLMod πΌ)) β β
)) |
25 | | eqid 2737 |
. . . . . . . . 9
β’ (π
unitVec πΌ) = (π
unitVec πΌ) |
26 | 25, 2, 5 | uvcff 21213 |
. . . . . . . 8
β’ ((π
β Ring β§ πΌ β Fin) β (π
unitVec πΌ):πΌβΆ(Baseβ(π
freeLMod πΌ))) |
27 | 1, 26 | sylan 581 |
. . . . . . 7
β’ ((π
β DivRing β§ πΌ β Fin) β (π
unitVec πΌ):πΌβΆ(Baseβ(π
freeLMod πΌ))) |
28 | 27 | frnd 6681 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin) β ran (π
unitVec πΌ) β (Baseβ(π
freeLMod πΌ))) |
29 | 28, 22 | sseqtrrdi 4000 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin) β ran (π
unitVec πΌ) β ((Baseβ(π
freeLMod πΌ)) β β
)) |
30 | 29 | 3adant3 1133 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β ran (π
unitVec πΌ) β ((Baseβ(π
freeLMod πΌ)) β β
)) |
31 | 5 | linds1 21232 |
. . . . . 6
β’ (π β (LIndSβ(π
freeLMod πΌ)) β π β (Baseβ(π
freeLMod πΌ))) |
32 | 31 | 3ad2ant3 1136 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β π β (Baseβ(π
freeLMod πΌ))) |
33 | | un0 4355 |
. . . . . . . 8
β’ (ran
(π
unitVec πΌ) βͺ β
) = ran (π
unitVec πΌ) |
34 | 33 | fveq2i 6850 |
. . . . . . 7
β’
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(ran (π
unitVec πΌ) βͺ β
)) =
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βran (π
unitVec πΌ)) |
35 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LSpanβ(π
freeLMod πΌ)) =
(LSpanβ(π
freeLMod
πΌ)) |
36 | 6, 35, 10 | mrclsp 20466 |
. . . . . . . . . 10
β’ ((π
freeLMod πΌ) β LMod β (LSpanβ(π
freeLMod πΌ)) = (mrClsβ(LSubSpβ(π
freeLMod πΌ)))) |
37 | 4, 36 | syl 17 |
. . . . . . . . 9
β’ ((π
β DivRing β§ πΌ β Fin) β
(LSpanβ(π
freeLMod
πΌ)) =
(mrClsβ(LSubSpβ(π
freeLMod πΌ)))) |
38 | 37 | fveq1d 6849 |
. . . . . . . 8
β’ ((π
β DivRing β§ πΌ β Fin) β
((LSpanβ(π
freeLMod
πΌ))βran (π
unitVec πΌ)) = ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βran (π
unitVec πΌ))) |
39 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LBasisβ(π
freeLMod πΌ)) =
(LBasisβ(π
freeLMod
πΌ)) |
40 | 2, 25, 39 | frlmlbs 21219 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΌ β Fin) β ran (π
unitVec πΌ) β (LBasisβ(π
freeLMod πΌ))) |
41 | 1, 40 | sylan 581 |
. . . . . . . . 9
β’ ((π
β DivRing β§ πΌ β Fin) β ran (π
unitVec πΌ) β (LBasisβ(π
freeLMod πΌ))) |
42 | 5, 39, 35 | lbssp 20556 |
. . . . . . . . 9
β’ (ran
(π
unitVec πΌ) β (LBasisβ(π
freeLMod πΌ)) β ((LSpanβ(π
freeLMod πΌ))βran (π
unitVec πΌ)) = (Baseβ(π
freeLMod πΌ))) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
β’ ((π
β DivRing β§ πΌ β Fin) β
((LSpanβ(π
freeLMod
πΌ))βran (π
unitVec πΌ)) = (Baseβ(π
freeLMod πΌ))) |
44 | 38, 43 | eqtr3d 2779 |
. . . . . . 7
β’ ((π
β DivRing β§ πΌ β Fin) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))βran (π
unitVec πΌ)) = (Baseβ(π
freeLMod πΌ))) |
45 | 34, 44 | eqtrid 2789 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(ran (π
unitVec πΌ) βͺ β
)) = (Baseβ(π
freeLMod πΌ))) |
46 | 45 | 3adant3 1133 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β
((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(ran (π
unitVec πΌ) βͺ β
)) = (Baseβ(π
freeLMod πΌ))) |
47 | 32, 46 | sseqtrrd 3990 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β π β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(ran (π
unitVec πΌ) βͺ β
))) |
48 | | un0 4355 |
. . . . 5
β’ (π βͺ β
) = π |
49 | | drngnzr 20748 |
. . . . . . . . . . . . 13
β’ (π
β DivRing β π
β NzRing) |
50 | 49 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π
β DivRing β§ πΌ β Fin) β π
β NzRing) |
51 | 12, 50 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ ((π
β DivRing β§ πΌ β Fin) β
(Scalarβ(π
freeLMod
πΌ)) β
NzRing) |
52 | 4, 51 | jca 513 |
. . . . . . . . . 10
β’ ((π
β DivRing β§ πΌ β Fin) β ((π
freeLMod πΌ) β LMod β§ (Scalarβ(π
freeLMod πΌ)) β NzRing)) |
53 | 35, 15 | lindsind2 21241 |
. . . . . . . . . . 11
β’ ((((π
freeLMod πΌ) β LMod β§ (Scalarβ(π
freeLMod πΌ)) β NzRing) β§ π β (LIndSβ(π
freeLMod πΌ)) β§ π¦ β π) β Β¬ π¦ β ((LSpanβ(π
freeLMod πΌ))β(π β {π¦}))) |
54 | 53 | 3expa 1119 |
. . . . . . . . . 10
β’
(((((π
freeLMod
πΌ) β LMod β§
(Scalarβ(π
freeLMod
πΌ)) β NzRing) β§
π β
(LIndSβ(π
freeLMod
πΌ))) β§ π¦ β π) β Β¬ π¦ β ((LSpanβ(π
freeLMod πΌ))β(π β {π¦}))) |
55 | 52, 54 | sylanl1 679 |
. . . . . . . . 9
β’ ((((π
β DivRing β§ πΌ β Fin) β§ π β (LIndSβ(π
freeLMod πΌ))) β§ π¦ β π) β Β¬ π¦ β ((LSpanβ(π
freeLMod πΌ))β(π β {π¦}))) |
56 | 37 | fveq1d 6849 |
. . . . . . . . . . 11
β’ ((π
β DivRing β§ πΌ β Fin) β
((LSpanβ(π
freeLMod
πΌ))β(π β {π¦})) = ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦}))) |
57 | 56 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((π
β DivRing β§ πΌ β Fin) β (π¦ β ((LSpanβ(π
freeLMod πΌ))β(π β {π¦})) β π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦})))) |
58 | 57 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π
β DivRing β§ πΌ β Fin) β§ π β (LIndSβ(π
freeLMod πΌ))) β§ π¦ β π) β (π¦ β ((LSpanβ(π
freeLMod πΌ))β(π β {π¦})) β π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦})))) |
59 | 55, 58 | mtbid 324 |
. . . . . . . 8
β’ ((((π
β DivRing β§ πΌ β Fin) β§ π β (LIndSβ(π
freeLMod πΌ))) β§ π¦ β π) β Β¬ π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦}))) |
60 | 59 | ralrimiva 3144 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β Fin) β§ π β (LIndSβ(π
freeLMod πΌ))) β βπ¦ β π Β¬ π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦}))) |
61 | 60 | 3impa 1111 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β βπ¦ β π Β¬ π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦}))) |
62 | 10, 11 | ismri2 17519 |
. . . . . . . 8
β’
(((LSubSpβ(π
freeLMod πΌ)) β
(Mooreβ(Baseβ(π
freeLMod πΌ))) β§ π β (Baseβ(π
freeLMod πΌ))) β (π β (mrIndβ(LSubSpβ(π
freeLMod πΌ))) β βπ¦ β π Β¬ π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦})))) |
63 | 8, 31, 62 | syl2an 597 |
. . . . . . 7
β’ (((π
β DivRing β§ πΌ β Fin) β§ π β (LIndSβ(π
freeLMod πΌ))) β (π β (mrIndβ(LSubSpβ(π
freeLMod πΌ))) β βπ¦ β π Β¬ π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦})))) |
64 | 63 | 3impa 1111 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β (π β (mrIndβ(LSubSpβ(π
freeLMod πΌ))) β βπ¦ β π Β¬ π¦ β ((mrClsβ(LSubSpβ(π
freeLMod πΌ)))β(π β {π¦})))) |
65 | 61, 64 | mpbird 257 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β π β (mrIndβ(LSubSpβ(π
freeLMod πΌ)))) |
66 | 48, 65 | eqeltrid 2842 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β (π βͺ β
) β
(mrIndβ(LSubSpβ(π
freeLMod πΌ)))) |
67 | | simpr 486 |
. . . . . . 7
β’ ((π
β DivRing β§ πΌ β Fin) β πΌ β Fin) |
68 | 25 | uvcendim 21269 |
. . . . . . . . 9
β’ ((π
β NzRing β§ πΌ β Fin) β πΌ β ran (π
unitVec πΌ)) |
69 | 49, 68 | sylan 581 |
. . . . . . . 8
β’ ((π
β DivRing β§ πΌ β Fin) β πΌ β ran (π
unitVec πΌ)) |
70 | | enfi 9141 |
. . . . . . . 8
β’ (πΌ β ran (π
unitVec πΌ) β (πΌ β Fin β ran (π
unitVec πΌ) β Fin)) |
71 | 69, 70 | syl 17 |
. . . . . . 7
β’ ((π
β DivRing β§ πΌ β Fin) β (πΌ β Fin β ran (π
unitVec πΌ) β Fin)) |
72 | 67, 71 | mpbid 231 |
. . . . . 6
β’ ((π
β DivRing β§ πΌ β Fin) β ran (π
unitVec πΌ) β Fin) |
73 | 72 | olcd 873 |
. . . . 5
β’ ((π
β DivRing β§ πΌ β Fin) β (π β Fin β¨ ran (π
unitVec πΌ) β Fin)) |
74 | 73 | 3adant3 1133 |
. . . 4
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β (π β Fin β¨ ran (π
unitVec πΌ) β Fin)) |
75 | 9, 10, 11, 21, 24, 30, 47, 66, 74 | mreexexd 17535 |
. . 3
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β βπ β π« ran (π
unitVec πΌ)(π β π β§ (π βͺ β
) β
(mrIndβ(LSubSpβ(π
freeLMod πΌ))))) |
76 | | simpl 484 |
. . . . 5
β’ ((π β π β§ (π βͺ β
) β
(mrIndβ(LSubSpβ(π
freeLMod πΌ)))) β π β π) |
77 | | ovex 7395 |
. . . . . . 7
β’ (π
unitVec πΌ) β V |
78 | 77 | rnex 7854 |
. . . . . 6
β’ ran
(π
unitVec πΌ) β V |
79 | | elpwi 4572 |
. . . . . 6
β’ (π β π« ran (π
unitVec πΌ) β π β ran (π
unitVec πΌ)) |
80 | | ssdomg 8947 |
. . . . . 6
β’ (ran
(π
unitVec πΌ) β V β (π β ran (π
unitVec πΌ) β π βΌ ran (π
unitVec πΌ))) |
81 | 78, 79, 80 | mpsyl 68 |
. . . . 5
β’ (π β π« ran (π
unitVec πΌ) β π βΌ ran (π
unitVec πΌ)) |
82 | | endomtr 8959 |
. . . . 5
β’ ((π β π β§ π βΌ ran (π
unitVec πΌ)) β π βΌ ran (π
unitVec πΌ)) |
83 | 76, 81, 82 | syl2anr 598 |
. . . 4
β’ ((π β π« ran (π
unitVec πΌ) β§ (π β π β§ (π βͺ β
) β
(mrIndβ(LSubSpβ(π
freeLMod πΌ))))) β π βΌ ran (π
unitVec πΌ)) |
84 | 83 | rexlimiva 3145 |
. . 3
β’
(βπ β
π« ran (π
unitVec
πΌ)(π β π β§ (π βͺ β
) β
(mrIndβ(LSubSpβ(π
freeLMod πΌ)))) β π βΌ ran (π
unitVec πΌ)) |
85 | 75, 84 | syl 17 |
. 2
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β π βΌ ran (π
unitVec πΌ)) |
86 | 69 | ensymd 8952 |
. . 3
β’ ((π
β DivRing β§ πΌ β Fin) β ran (π
unitVec πΌ) β πΌ) |
87 | 86 | 3adant3 1133 |
. 2
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β ran (π
unitVec πΌ) β πΌ) |
88 | | domentr 8960 |
. 2
β’ ((π βΌ ran (π
unitVec πΌ) β§ ran (π
unitVec πΌ) β πΌ) β π βΌ πΌ) |
89 | 85, 87, 88 | syl2anc 585 |
1
β’ ((π
β DivRing β§ πΌ β Fin β§ π β (LIndSβ(π
freeLMod πΌ))) β π βΌ πΌ) |