Step | Hyp | Ref
| Expression |
1 | | lssacs.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
2 | | lssacs.s |
. . . . . 6
β’ π = (LSubSpβπ) |
3 | 1, 2 | lssss 20412 |
. . . . 5
β’ (π β π β π β π΅) |
4 | 3 | a1i 11 |
. . . 4
β’ (π β LMod β (π β π β π β π΅)) |
5 | | inss2 4190 |
. . . . . . . 8
β’
((SubGrpβπ)
β© {π β π«
π΅ β£ βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} |
6 | | ssrab2 4038 |
. . . . . . . 8
β’ {π β π« π΅ β£ βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β π« π΅ |
7 | 5, 6 | sstri 3954 |
. . . . . . 7
β’
((SubGrpβπ)
β© {π β π«
π΅ β£ βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β π« π΅ |
8 | 7 | sseli 3941 |
. . . . . 6
β’ (π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β π β π« π΅) |
9 | 8 | elpwid 4570 |
. . . . 5
β’ (π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β π β π΅) |
10 | 9 | a1i 11 |
. . . 4
β’ (π β LMod β (π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β π β π΅)) |
11 | | eqid 2733 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
13 | | eqid 2733 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
14 | 11, 12, 1, 13, 2 | islss4 20438 |
. . . . . . . 8
β’ (π β LMod β (π β π β (π β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π))) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β (π β π β (π β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π))) |
16 | | velpw 4566 |
. . . . . . . . . 10
β’ (π β π« π΅ β π β π΅) |
17 | | eleq2w 2818 |
. . . . . . . . . . . . 13
β’ (π = π β ((π₯( Β·π
βπ)π¦) β π β (π₯( Β·π
βπ)π¦) β π)) |
18 | 17 | raleqbi1dv 3306 |
. . . . . . . . . . . 12
β’ (π = π β (βπ¦ β π (π₯( Β·π
βπ)π¦) β π β βπ¦ β π (π₯( Β·π
βπ)π¦) β π)) |
19 | 18 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π = π β (βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π)) |
20 | 19 | elrab3 3647 |
. . . . . . . . . 10
β’ (π β π« π΅ β (π β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π)) |
21 | 16, 20 | sylbir 234 |
. . . . . . . . 9
β’ (π β π΅ β (π β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π)) |
22 | 21 | adantl 483 |
. . . . . . . 8
β’ ((π β LMod β§ π β π΅) β (π β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π)) |
23 | 22 | anbi2d 630 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β ((π β (SubGrpβπ) β§ π β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β (π β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π))) |
24 | 15, 23 | bitr4d 282 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β (π β π β (π β (SubGrpβπ) β§ π β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}))) |
25 | | elin 3927 |
. . . . . 6
β’ (π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β (π β (SubGrpβπ) β§ π β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π})) |
26 | 24, 25 | bitr4di 289 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (π β π β π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}))) |
27 | 26 | ex 414 |
. . . 4
β’ (π β LMod β (π β π΅ β (π β π β π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π})))) |
28 | 4, 10, 27 | pm5.21ndd 381 |
. . 3
β’ (π β LMod β (π β π β π β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}))) |
29 | 28 | eqrdv 2731 |
. 2
β’ (π β LMod β π = ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π})) |
30 | 1 | fvexi 6857 |
. . . 4
β’ π΅ β V |
31 | | mreacs 17543 |
. . . 4
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
32 | 30, 31 | mp1i 13 |
. . 3
β’ (π β LMod β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
33 | | lmodgrp 20343 |
. . . 4
β’ (π β LMod β π β Grp) |
34 | 1 | subgacs 18968 |
. . . 4
β’ (π β Grp β
(SubGrpβπ) β
(ACSβπ΅)) |
35 | 33, 34 | syl 17 |
. . 3
β’ (π β LMod β
(SubGrpβπ) β
(ACSβπ΅)) |
36 | 1, 11, 13, 12 | lmodvscl 20354 |
. . . . . 6
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅) β (π₯( Β·π
βπ)π¦) β π΅) |
37 | 36 | 3expb 1121 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅)) β (π₯( Β·π
βπ)π¦) β π΅) |
38 | 37 | ralrimivva 3194 |
. . . 4
β’ (π β LMod β
βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π΅ (π₯( Β·π
βπ)π¦) β π΅) |
39 | | acsfn1c 17547 |
. . . 4
β’ ((π΅ β V β§ βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π΅ (π₯( Β·π
βπ)π¦) β π΅) β {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β (ACSβπ΅)) |
40 | 30, 38, 39 | sylancr 588 |
. . 3
β’ (π β LMod β {π β π« π΅ β£ βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β (ACSβπ΅)) |
41 | | mreincl 17484 |
. . 3
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ (SubGrpβπ) β (ACSβπ΅) β§ {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π} β (ACSβπ΅)) β ((SubGrpβπ) β© {π β π« π΅ β£ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β (ACSβπ΅)) |
42 | 32, 35, 40, 41 | syl3anc 1372 |
. 2
β’ (π β LMod β
((SubGrpβπ) β©
{π β π« π΅ β£ βπ₯ β
(Baseβ(Scalarβπ))βπ¦ β π (π₯( Β·π
βπ)π¦) β π}) β (ACSβπ΅)) |
43 | 29, 42 | eqeltrd 2834 |
1
β’ (π β LMod β π β (ACSβπ΅)) |