Step | Hyp | Ref
| Expression |
1 | | dsmmlss.p |
. . 3
β’ π = (πXsπ
) |
2 | | dsmmlss.h |
. . 3
β’ π» = (Baseβ(π βm π
)) |
3 | | dsmmlss.i |
. . 3
β’ (π β πΌ β π) |
4 | | dsmmlss.s |
. . 3
β’ (π β π β Ring) |
5 | | dsmmlss.r |
. . . 4
β’ (π β π
:πΌβΆLMod) |
6 | | lmodgrp 20470 |
. . . . 5
β’ (π β LMod β π β Grp) |
7 | 6 | ssriv 3985 |
. . . 4
β’ LMod
β Grp |
8 | | fss 6731 |
. . . 4
β’ ((π
:πΌβΆLMod β§ LMod β Grp) β
π
:πΌβΆGrp) |
9 | 5, 7, 8 | sylancl 586 |
. . 3
β’ (π β π
:πΌβΆGrp) |
10 | 1, 2, 3, 4, 9 | dsmmsubg 21289 |
. 2
β’ (π β π» β (SubGrpβπ)) |
11 | | dsmmlss.k |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (Scalarβ(π
βπ₯)) = π) |
12 | 1, 4, 3, 5, 11 | prdslmodd 20572 |
. . . . . 6
β’ (π β π β LMod) |
13 | 12 | adantr 481 |
. . . . 5
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β π β LMod) |
14 | | simprl 769 |
. . . . 5
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β π β (Baseβ(Scalarβπ))) |
15 | | simprr 771 |
. . . . . . 7
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β π β π») |
16 | | eqid 2732 |
. . . . . . . . 9
β’ (π βm π
) = (π βm π
) |
17 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
18 | 5 | ffnd 6715 |
. . . . . . . . 9
β’ (π β π
Fn πΌ) |
19 | 1, 16, 17, 2, 3, 18 | dsmmelbas 21285 |
. . . . . . . 8
β’ (π β (π β π» β (π β (Baseβπ) β§ {π₯ β πΌ β£ (πβπ₯) β (0gβ(π
βπ₯))} β Fin))) |
20 | 19 | adantr 481 |
. . . . . . 7
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β (π β π» β (π β (Baseβπ) β§ {π₯ β πΌ β£ (πβπ₯) β (0gβ(π
βπ₯))} β Fin))) |
21 | 15, 20 | mpbid 231 |
. . . . . 6
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β (π β (Baseβπ) β§ {π₯ β πΌ β£ (πβπ₯) β (0gβ(π
βπ₯))} β Fin)) |
22 | 21 | simpld 495 |
. . . . 5
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β π β (Baseβπ)) |
23 | | eqid 2732 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
24 | | eqid 2732 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
25 | | eqid 2732 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
26 | 17, 23, 24, 25 | lmodvscl 20481 |
. . . . 5
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ π β (Baseβπ)) β (π( Β·π
βπ)π) β (Baseβπ)) |
27 | 13, 14, 22, 26 | syl3anc 1371 |
. . . 4
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β (π( Β·π
βπ)π) β (Baseβπ)) |
28 | 21 | simprd 496 |
. . . . 5
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β {π₯ β πΌ β£ (πβπ₯) β (0gβ(π
βπ₯))} β Fin) |
29 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
30 | 4 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π β Ring) |
31 | 3 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β πΌ β π) |
32 | 18 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π
Fn πΌ) |
33 | 5, 3 | fexd 7225 |
. . . . . . . . . . . . . . . . 17
β’ (π β π
β V) |
34 | 1, 4, 33 | prdssca 17398 |
. . . . . . . . . . . . . . . 16
β’ (π β π = (Scalarβπ)) |
35 | 34 | fveq2d 6892 |
. . . . . . . . . . . . . . 15
β’ (π β (Baseβπ) =
(Baseβ(Scalarβπ))) |
36 | 35 | eleq2d 2819 |
. . . . . . . . . . . . . 14
β’ (π β (π β (Baseβπ) β π β (Baseβ(Scalarβπ)))) |
37 | 36 | biimpar 478 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (Baseβ(Scalarβπ))) β π β (Baseβπ)) |
38 | 37 | adantrr 715 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β π β (Baseβπ)) |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π β (Baseβπ)) |
40 | 22 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π β (Baseβπ)) |
41 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π₯ β πΌ) |
42 | 1, 17, 24, 29, 30, 31, 32, 39, 40, 41 | prdsvscafval 17422 |
. . . . . . . . . 10
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β ((π( Β·π
βπ)π)βπ₯) = (π( Β·π
β(π
βπ₯))(πβπ₯))) |
43 | 42 | adantrr 715 |
. . . . . . . . 9
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ (π₯ β πΌ β§ (πβπ₯) = (0gβ(π
βπ₯)))) β ((π( Β·π
βπ)π)βπ₯) = (π( Β·π
β(π
βπ₯))(πβπ₯))) |
44 | 5 | ffvelcdmda 7083 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΌ) β (π
βπ₯) β LMod) |
45 | 44 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β (π
βπ₯) β LMod) |
46 | | simplrl 775 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π β (Baseβ(Scalarβπ))) |
47 | 34 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β πΌ) β π = (Scalarβπ)) |
48 | 11, 47 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΌ) β (Scalarβ(π
βπ₯)) = (Scalarβπ)) |
49 | 48 | fveq2d 6892 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΌ) β (Baseβ(Scalarβ(π
βπ₯))) = (Baseβ(Scalarβπ))) |
50 | 49 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β (Baseβ(Scalarβ(π
βπ₯))) = (Baseβ(Scalarβπ))) |
51 | 46, 50 | eleqtrrd 2836 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β π β (Baseβ(Scalarβ(π
βπ₯)))) |
52 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Scalarβ(π
βπ₯)) = (Scalarβ(π
βπ₯)) |
53 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (
Β·π β(π
βπ₯)) = ( Β·π
β(π
βπ₯)) |
54 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβ(Scalarβ(π
βπ₯))) = (Baseβ(Scalarβ(π
βπ₯))) |
55 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(0gβ(π
βπ₯)) = (0gβ(π
βπ₯)) |
56 | 52, 53, 54, 55 | lmodvs0 20498 |
. . . . . . . . . . . 12
β’ (((π
βπ₯) β LMod β§ π β (Baseβ(Scalarβ(π
βπ₯)))) β (π( Β·π
β(π
βπ₯))(0gβ(π
βπ₯))) = (0gβ(π
βπ₯))) |
57 | 45, 51, 56 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β (π( Β·π
β(π
βπ₯))(0gβ(π
βπ₯))) = (0gβ(π
βπ₯))) |
58 | | oveq2 7413 |
. . . . . . . . . . . 12
β’ ((πβπ₯) = (0gβ(π
βπ₯)) β (π( Β·π
β(π
βπ₯))(πβπ₯)) = (π( Β·π
β(π
βπ₯))(0gβ(π
βπ₯)))) |
59 | 58 | eqeq1d 2734 |
. . . . . . . . . . 11
β’ ((πβπ₯) = (0gβ(π
βπ₯)) β ((π( Β·π
β(π
βπ₯))(πβπ₯)) = (0gβ(π
βπ₯)) β (π( Β·π
β(π
βπ₯))(0gβ(π
βπ₯))) = (0gβ(π
βπ₯)))) |
60 | 57, 59 | syl5ibrcom 246 |
. . . . . . . . . 10
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β ((πβπ₯) = (0gβ(π
βπ₯)) β (π( Β·π
β(π
βπ₯))(πβπ₯)) = (0gβ(π
βπ₯)))) |
61 | 60 | impr 455 |
. . . . . . . . 9
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ (π₯ β πΌ β§ (πβπ₯) = (0gβ(π
βπ₯)))) β (π( Β·π
β(π
βπ₯))(πβπ₯)) = (0gβ(π
βπ₯))) |
62 | 43, 61 | eqtrd 2772 |
. . . . . . . 8
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ (π₯ β πΌ β§ (πβπ₯) = (0gβ(π
βπ₯)))) β ((π( Β·π
βπ)π)βπ₯) = (0gβ(π
βπ₯))) |
63 | 62 | expr 457 |
. . . . . . 7
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β ((πβπ₯) = (0gβ(π
βπ₯)) β ((π( Β·π
βπ)π)βπ₯) = (0gβ(π
βπ₯)))) |
64 | 63 | necon3d 2961 |
. . . . . 6
β’ (((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β§ π₯ β πΌ) β (((π( Β·π
βπ)π)βπ₯) β (0gβ(π
βπ₯)) β (πβπ₯) β (0gβ(π
βπ₯)))) |
65 | 64 | ss2rabdv 4072 |
. . . . 5
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β {π₯ β πΌ β£ ((π( Β·π
βπ)π)βπ₯) β (0gβ(π
βπ₯))} β {π₯ β πΌ β£ (πβπ₯) β (0gβ(π
βπ₯))}) |
66 | 28, 65 | ssfid 9263 |
. . . 4
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β {π₯ β πΌ β£ ((π( Β·π
βπ)π)βπ₯) β (0gβ(π
βπ₯))} β Fin) |
67 | 1, 16, 17, 2, 3, 18 | dsmmelbas 21285 |
. . . . 5
β’ (π β ((π( Β·π
βπ)π) β π» β ((π( Β·π
βπ)π) β (Baseβπ) β§ {π₯ β πΌ β£ ((π( Β·π
βπ)π)βπ₯) β (0gβ(π
βπ₯))} β Fin))) |
68 | 67 | adantr 481 |
. . . 4
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β ((π( Β·π
βπ)π) β π» β ((π( Β·π
βπ)π) β (Baseβπ) β§ {π₯ β πΌ β£ ((π( Β·π
βπ)π)βπ₯) β (0gβ(π
βπ₯))} β Fin))) |
69 | 27, 66, 68 | mpbir2and 711 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π»)) β (π( Β·π
βπ)π) β π») |
70 | 69 | ralrimivva 3200 |
. 2
β’ (π β βπ β (Baseβ(Scalarβπ))βπ β π» (π( Β·π
βπ)π) β π») |
71 | | dsmmlss.u |
. . . 4
β’ π = (LSubSpβπ) |
72 | 23, 25, 17, 24, 71 | islss4 20565 |
. . 3
β’ (π β LMod β (π» β π β (π» β (SubGrpβπ) β§ βπ β (Baseβ(Scalarβπ))βπ β π» (π( Β·π
βπ)π) β π»))) |
73 | 12, 72 | syl 17 |
. 2
β’ (π β (π» β π β (π» β (SubGrpβπ) β§ βπ β (Baseβ(Scalarβπ))βπ β π» (π( Β·π
βπ)π) β π»))) |
74 | 10, 70, 73 | mpbir2and 711 |
1
β’ (π β π» β π) |