Step | Hyp | Ref
| Expression |
1 | | lssdimle.x |
. . . . 5
β’ π = (π βΎs π) |
2 | | eqid 2737 |
. . . . 5
β’
(LSubSpβπ) =
(LSubSpβπ) |
3 | 1, 2 | lsslvec 20584 |
. . . 4
β’ ((π β LVec β§ π β (LSubSpβπ)) β π β LVec) |
4 | | eqid 2737 |
. . . . 5
β’
(LBasisβπ) =
(LBasisβπ) |
5 | 4 | lbsex 20642 |
. . . 4
β’ (π β LVec β
(LBasisβπ) β
β
) |
6 | 3, 5 | syl 17 |
. . 3
β’ ((π β LVec β§ π β (LSubSpβπ)) β (LBasisβπ) β β
) |
7 | | n0 4311 |
. . 3
β’
((LBasisβπ)
β β
β βπ₯ π₯ β (LBasisβπ)) |
8 | 6, 7 | sylib 217 |
. 2
β’ ((π β LVec β§ π β (LSubSpβπ)) β βπ₯ π₯ β (LBasisβπ)) |
9 | | hashss 14316 |
. . . . 5
β’ ((π€ β (LBasisβπ) β§ π₯ β π€) β (β―βπ₯) β€ (β―βπ€)) |
10 | 9 | adantll 713 |
. . . 4
β’
(((((π β LVec
β§ π β
(LSubSpβπ)) β§
π₯ β
(LBasisβπ)) β§
π€ β
(LBasisβπ)) β§
π₯ β π€) β (β―βπ₯) β€ (β―βπ€)) |
11 | 4 | dimval 32340 |
. . . . . 6
β’ ((π β LVec β§ π₯ β (LBasisβπ)) β (dimβπ) = (β―βπ₯)) |
12 | 3, 11 | sylan 581 |
. . . . 5
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β (dimβπ) = (β―βπ₯)) |
13 | 12 | ad2antrr 725 |
. . . 4
β’
(((((π β LVec
β§ π β
(LSubSpβπ)) β§
π₯ β
(LBasisβπ)) β§
π€ β
(LBasisβπ)) β§
π₯ β π€) β (dimβπ) = (β―βπ₯)) |
14 | | eqid 2737 |
. . . . . 6
β’
(LBasisβπ) =
(LBasisβπ) |
15 | 14 | dimval 32340 |
. . . . 5
β’ ((π β LVec β§ π€ β (LBasisβπ)) β (dimβπ) = (β―βπ€)) |
16 | 15 | ad5ant14 757 |
. . . 4
β’
(((((π β LVec
β§ π β
(LSubSpβπ)) β§
π₯ β
(LBasisβπ)) β§
π€ β
(LBasisβπ)) β§
π₯ β π€) β (dimβπ) = (β―βπ€)) |
17 | 10, 13, 16 | 3brtr4d 5142 |
. . 3
β’
(((((π β LVec
β§ π β
(LSubSpβπ)) β§
π₯ β
(LBasisβπ)) β§
π€ β
(LBasisβπ)) β§
π₯ β π€) β (dimβπ) β€ (dimβπ)) |
18 | | simpll 766 |
. . . 4
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π β LVec) |
19 | | lveclmod 20583 |
. . . . . 6
β’ (π β LVec β π β LMod) |
20 | 19 | ad2antrr 725 |
. . . . 5
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π β LMod) |
21 | | simplr 768 |
. . . . 5
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π β (LSubSpβπ)) |
22 | | simpr 486 |
. . . . . . 7
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π₯ β (LBasisβπ)) |
23 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
24 | 23, 4 | lbsss 20554 |
. . . . . . 7
β’ (π₯ β (LBasisβπ) β π₯ β (Baseβπ)) |
25 | 22, 24 | syl 17 |
. . . . . 6
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π₯ β (Baseβπ)) |
26 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
27 | 26, 2 | lssss 20413 |
. . . . . . 7
β’ (π β (LSubSpβπ) β π β (Baseβπ)) |
28 | 1, 26 | ressbas2 17127 |
. . . . . . 7
β’ (π β (Baseβπ) β π = (Baseβπ)) |
29 | 21, 27, 28 | 3syl 18 |
. . . . . 6
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π = (Baseβπ)) |
30 | 25, 29 | sseqtrrd 3990 |
. . . . 5
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π₯ β π) |
31 | 4 | lbslinds 21255 |
. . . . . 6
β’
(LBasisβπ)
β (LIndSβπ) |
32 | 31, 22 | sselid 3947 |
. . . . 5
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π₯ β (LIndSβπ)) |
33 | 2, 1 | lsslinds 21253 |
. . . . . 6
β’ ((π β LMod β§ π β (LSubSpβπ) β§ π₯ β π) β (π₯ β (LIndSβπ) β π₯ β (LIndSβπ))) |
34 | 33 | biimpa 478 |
. . . . 5
β’ (((π β LMod β§ π β (LSubSpβπ) β§ π₯ β π) β§ π₯ β (LIndSβπ)) β π₯ β (LIndSβπ)) |
35 | 20, 21, 30, 32, 34 | syl31anc 1374 |
. . . 4
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β π₯ β (LIndSβπ)) |
36 | 14 | islinds4 21257 |
. . . . 5
β’ (π β LVec β (π₯ β (LIndSβπ) β βπ€ β (LBasisβπ)π₯ β π€)) |
37 | 36 | biimpa 478 |
. . . 4
β’ ((π β LVec β§ π₯ β (LIndSβπ)) β βπ€ β (LBasisβπ)π₯ β π€) |
38 | 18, 35, 37 | syl2anc 585 |
. . 3
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β βπ€ β (LBasisβπ)π₯ β π€) |
39 | 17, 38 | r19.29a 3160 |
. 2
β’ (((π β LVec β§ π β (LSubSpβπ)) β§ π₯ β (LBasisβπ)) β (dimβπ) β€ (dimβπ)) |
40 | 8, 39 | exlimddv 1939 |
1
β’ ((π β LVec β§ π β (LSubSpβπ)) β (dimβπ) β€ (dimβπ)) |