Step | Hyp | Ref
| Expression |
1 | | quslmod.n |
. . . 4
β’ π = (π /s (π ~QG πΊ)) |
2 | 1 | a1i 11 |
. . 3
β’ (π β π = (π /s (π ~QG πΊ))) |
3 | | quslmod.v |
. . . 4
β’ π = (Baseβπ) |
4 | 3 | a1i 11 |
. . 3
β’ (π β π = (Baseβπ)) |
5 | | eqid 2733 |
. . 3
β’ (π₯ β π β¦ [π₯](π ~QG πΊ)) = (π₯ β π β¦ [π₯](π ~QG πΊ)) |
6 | | ovexd 7393 |
. . 3
β’ (π β (π ~QG πΊ) β V) |
7 | | quslmod.1 |
. . 3
β’ (π β π β LMod) |
8 | 2, 4, 5, 6, 7 | qusval 17429 |
. 2
β’ (π β π = ((π₯ β π β¦ [π₯](π ~QG πΊ)) βs π)) |
9 | | eqid 2733 |
. 2
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
10 | | eqid 2733 |
. 2
β’
(+gβπ) = (+gβπ) |
11 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
12 | | eqid 2733 |
. 2
β’
(0gβπ) = (0gβπ) |
13 | 2, 4, 5, 6, 7 | quslem 17430 |
. 2
β’ (π β (π₯ β π β¦ [π₯](π ~QG πΊ)):πβontoβ(π / (π ~QG πΊ))) |
14 | | quslmod.2 |
. . . . 5
β’ (π β πΊ β (LSubSpβπ)) |
15 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
16 | 15 | lsssubg 20433 |
. . . . 5
β’ ((π β LMod β§ πΊ β (LSubSpβπ)) β πΊ β (SubGrpβπ)) |
17 | 7, 14, 16 | syl2anc 585 |
. . . 4
β’ (π β πΊ β (SubGrpβπ)) |
18 | | eqid 2733 |
. . . . 5
β’ (π ~QG πΊ) = (π ~QG πΊ) |
19 | 3, 18 | eqger 18985 |
. . . 4
β’ (πΊ β (SubGrpβπ) β (π ~QG πΊ) Er π) |
20 | 17, 19 | syl 17 |
. . 3
β’ (π β (π ~QG πΊ) Er π) |
21 | 3 | fvexi 6857 |
. . . 4
β’ π β V |
22 | 21 | a1i 11 |
. . 3
β’ (π β π β V) |
23 | | lmodgrp 20343 |
. . . . . 6
β’ (π β LMod β π β Grp) |
24 | 7, 23 | syl 17 |
. . . . 5
β’ (π β π β Grp) |
25 | 24 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β π β Grp) |
26 | | simprl 770 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β π β π) |
27 | | simprr 772 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β π β π) |
28 | 3, 10 | grpcl 18761 |
. . . 4
β’ ((π β Grp β§ π β π β§ π β π) β (π(+gβπ)π) β π) |
29 | 25, 26, 27, 28 | syl3anc 1372 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β (π(+gβπ)π) β π) |
30 | | lmodabl 20384 |
. . . . . 6
β’ (π β LMod β π β Abel) |
31 | | ablnsg 19630 |
. . . . . 6
β’ (π β Abel β
(NrmSGrpβπ) =
(SubGrpβπ)) |
32 | 7, 30, 31 | 3syl 18 |
. . . . 5
β’ (π β (NrmSGrpβπ) = (SubGrpβπ)) |
33 | 17, 32 | eleqtrrd 2837 |
. . . 4
β’ (π β πΊ β (NrmSGrpβπ)) |
34 | 3, 18, 10 | eqgcpbl 18989 |
. . . 4
β’ (πΊ β (NrmSGrpβπ) β ((π(π ~QG πΊ)π β§ π(π ~QG πΊ)π) β (π(+gβπ)π)(π ~QG πΊ)(π(+gβπ)π))) |
35 | 33, 34 | syl 17 |
. . 3
β’ (π β ((π(π ~QG πΊ)π β§ π(π ~QG πΊ)π) β (π(+gβπ)π)(π ~QG πΊ)(π(+gβπ)π))) |
36 | 20, 22, 5, 29, 35 | ercpbl 17436 |
. 2
β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β ((((π₯ β π β¦ [π₯](π ~QG πΊ))βπ) = ((π₯ β π β¦ [π₯](π ~QG πΊ))βπ) β§ ((π₯ β π β¦ [π₯](π ~QG πΊ))βπ) = ((π₯ β π β¦ [π₯](π ~QG πΊ))βπ)) β ((π₯ β π β¦ [π₯](π ~QG πΊ))β(π(+gβπ)π)) = ((π₯ β π β¦ [π₯](π ~QG πΊ))β(π(+gβπ)π)))) |
37 | 7 | adantr 482 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β LMod) |
38 | 14 | adantr 482 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β πΊ β (LSubSpβπ)) |
39 | | simpr1 1195 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β (Baseβ(Scalarβπ))) |
40 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
41 | | simpr2 1196 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
42 | | simpr3 1197 |
. . 3
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
43 | 3, 18, 9, 11, 37, 38, 39, 1, 40, 5, 41, 42 | qusvscpbl 32190 |
. 2
β’ ((π β§ (π β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β (((π₯ β π β¦ [π₯](π ~QG πΊ))βπ) = ((π₯ β π β¦ [π₯](π ~QG πΊ))βπ) β ((π₯ β π β¦ [π₯](π ~QG πΊ))β(π( Β·π
βπ)π)) = ((π₯ β π β¦ [π₯](π ~QG πΊ))β(π( Β·π
βπ)π)))) |
44 | 8, 3, 9, 10, 11, 12, 13, 36, 43, 7 | imaslmod 32192 |
1
β’ (π β π β LMod) |