Step | Hyp | Ref
| Expression |
1 | | islss3.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | islss3.s |
. . . . 5
β’ π = (LSubSpβπ) |
3 | 1, 2 | lssss 20413 |
. . . 4
β’ (π β π β π β π) |
4 | 3 | adantl 483 |
. . 3
β’ ((π β LMod β§ π β π) β π β π) |
5 | | islss3.x |
. . . . . . 7
β’ π = (π βΎs π) |
6 | 5, 1 | ressbas2 17127 |
. . . . . 6
β’ (π β π β π = (Baseβπ)) |
7 | 6 | adantl 483 |
. . . . 5
β’ ((π β LMod β§ π β π) β π = (Baseβπ)) |
8 | 3, 7 | sylan2 594 |
. . . 4
β’ ((π β LMod β§ π β π) β π = (Baseβπ)) |
9 | | eqid 2737 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
10 | 5, 9 | ressplusg 17178 |
. . . . 5
β’ (π β π β (+gβπ) = (+gβπ)) |
11 | 10 | adantl 483 |
. . . 4
β’ ((π β LMod β§ π β π) β (+gβπ) = (+gβπ)) |
12 | | eqid 2737 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
13 | 5, 12 | resssca 17231 |
. . . . 5
β’ (π β π β (Scalarβπ) = (Scalarβπ)) |
14 | 13 | adantl 483 |
. . . 4
β’ ((π β LMod β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
15 | | eqid 2737 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
16 | 5, 15 | ressvsca 17232 |
. . . . 5
β’ (π β π β (
Β·π βπ) = ( Β·π
βπ)) |
17 | 16 | adantl 483 |
. . . 4
β’ ((π β LMod β§ π β π) β (
Β·π βπ) = ( Β·π
βπ)) |
18 | | eqidd 2738 |
. . . 4
β’ ((π β LMod β§ π β π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
19 | | eqidd 2738 |
. . . 4
β’ ((π β LMod β§ π β π) β
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ))) |
20 | | eqidd 2738 |
. . . 4
β’ ((π β LMod β§ π β π) β
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ))) |
21 | | eqidd 2738 |
. . . 4
β’ ((π β LMod β§ π β π) β
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ))) |
22 | 12 | lmodring 20346 |
. . . . 5
β’ (π β LMod β
(Scalarβπ) β
Ring) |
23 | 22 | adantr 482 |
. . . 4
β’ ((π β LMod β§ π β π) β (Scalarβπ) β Ring) |
24 | 2 | lsssubg 20434 |
. . . . 5
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
25 | 5 | subggrp 18938 |
. . . . 5
β’ (π β (SubGrpβπ) β π β Grp) |
26 | 24, 25 | syl 17 |
. . . 4
β’ ((π β LMod β§ π β π) β π β Grp) |
27 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
28 | 12, 15, 27, 2 | lssvscl 20432 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π)) β (π₯( Β·π
βπ)π) β π) |
29 | 28 | 3impb 1116 |
. . . 4
β’ (((π β LMod β§ π β π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π β π) β (π₯( Β·π
βπ)π) β π) |
30 | | simpll 766 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β LMod) |
31 | | simpr1 1195 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π₯ β (Baseβ(Scalarβπ))) |
32 | 3 | ad2antlr 726 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
33 | | simpr2 1196 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
34 | 32, 33 | sseldd 3950 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
35 | | simpr3 1197 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
36 | 32, 35 | sseldd 3950 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β π β π) |
37 | 1, 9, 12, 15, 27 | lmodvsdi 20361 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β (π₯( Β·π
βπ)(π(+gβπ)π)) = ((π₯( Β·π
βπ)π)(+gβπ)(π₯( Β·π
βπ)π))) |
38 | 30, 31, 34, 36, 37 | syl13anc 1373 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β π β§ π β π)) β (π₯( Β·π
βπ)(π(+gβπ)π)) = ((π₯( Β·π
βπ)π)(+gβπ)(π₯( Β·π
βπ)π))) |
39 | | simpll 766 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β π β LMod) |
40 | | simpr1 1195 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β π₯ β (Baseβ(Scalarβπ))) |
41 | | simpr2 1196 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β π β (Baseβ(Scalarβπ))) |
42 | 3 | ad2antlr 726 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β π β π) |
43 | | simpr3 1197 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β π β π) |
44 | 42, 43 | sseldd 3950 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β π β π) |
45 | | eqid 2737 |
. . . . . 6
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
46 | 1, 9, 12, 15, 27, 45 | lmodvsdir 20362 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π) = ((π₯( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π))) |
47 | 39, 40, 41, 44, 46 | syl13anc 1373 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π) = ((π₯( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π))) |
48 | | eqid 2737 |
. . . . . 6
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
49 | 1, 12, 15, 27, 48 | lmodvsass 20363 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β ((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π) = (π₯( Β·π
βπ)(π(
Β·π βπ)π))) |
50 | 39, 40, 41, 44, 49 | syl13anc 1373 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ)) β§ π β π)) β ((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π) = (π₯( Β·π
βπ)(π(
Β·π βπ)π))) |
51 | 4 | sselda 3949 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ π₯ β π) β π₯ β π) |
52 | | eqid 2737 |
. . . . . . 7
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
53 | 1, 12, 15, 52 | lmodvs1 20366 |
. . . . . 6
β’ ((π β LMod β§ π₯ β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π₯) = π₯) |
54 | 53 | adantlr 714 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ π₯ β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π₯) = π₯) |
55 | 51, 54 | syldan 592 |
. . . 4
β’ (((π β LMod β§ π β π) β§ π₯ β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π₯) = π₯) |
56 | 8, 11, 14, 17, 18, 19, 20, 21, 23, 26, 29, 38, 47, 50, 55 | islmodd 20344 |
. . 3
β’ ((π β LMod β§ π β π) β π β LMod) |
57 | 4, 56 | jca 513 |
. 2
β’ ((π β LMod β§ π β π) β (π β π β§ π β LMod)) |
58 | | simprl 770 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π β π) |
59 | 58, 6 | syl 17 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π = (Baseβπ)) |
60 | | fvex 6860 |
. . . . . . 7
β’
(Baseβπ)
β V |
61 | 59, 60 | eqeltrdi 2846 |
. . . . . 6
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π β V) |
62 | 5, 12 | resssca 17231 |
. . . . . 6
β’ (π β V β
(Scalarβπ) =
(Scalarβπ)) |
63 | 61, 62 | syl 17 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (Scalarβπ) = (Scalarβπ)) |
64 | 63 | eqcomd 2743 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (Scalarβπ) = (Scalarβπ)) |
65 | | eqidd 2738 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ))) |
66 | 1 | a1i 11 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π = (Baseβπ)) |
67 | 5, 9 | ressplusg 17178 |
. . . . . 6
β’ (π β V β
(+gβπ) =
(+gβπ)) |
68 | 61, 67 | syl 17 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β LMod)) β
(+gβπ) =
(+gβπ)) |
69 | 68 | eqcomd 2743 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β
(+gβπ) =
(+gβπ)) |
70 | 5, 15 | ressvsca 17232 |
. . . . . 6
β’ (π β V β (
Β·π βπ) = ( Β·π
βπ)) |
71 | 61, 70 | syl 17 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (
Β·π βπ) = ( Β·π
βπ)) |
72 | 71 | eqcomd 2743 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (
Β·π βπ) = ( Β·π
βπ)) |
73 | 2 | a1i 11 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π = (LSubSpβπ)) |
74 | 59, 58 | eqsstrrd 3988 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (Baseβπ) β π) |
75 | | lmodgrp 20345 |
. . . . . 6
β’ (π β LMod β π β Grp) |
76 | 75 | ad2antll 728 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π β Grp) |
77 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
78 | 77 | grpbn0 18786 |
. . . . 5
β’ (π β Grp β
(Baseβπ) β
β
) |
79 | 76, 78 | syl 17 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (Baseβπ) β β
) |
80 | | eqid 2737 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
81 | 77, 80 | lss1 20415 |
. . . . . 6
β’ (π β LMod β
(Baseβπ) β
(LSubSpβπ)) |
82 | 81 | ad2antll 728 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (Baseβπ) β (LSubSpβπ)) |
83 | | eqid 2737 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
84 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
85 | | eqid 2737 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
86 | | eqid 2737 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
87 | 83, 84, 85, 86, 80 | lsscl 20419 |
. . . . 5
β’
(((Baseβπ)
β (LSubSpβπ)
β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π₯( Β·π
βπ)π)(+gβπ)π) β (Baseβπ)) |
88 | 82, 87 | sylan 581 |
. . . 4
β’ (((π β LMod β§ (π β π β§ π β LMod)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π₯( Β·π
βπ)π)(+gβπ)π) β (Baseβπ)) |
89 | 64, 65, 66, 69, 72, 73, 74, 79, 88 | islssd 20412 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β LMod)) β (Baseβπ) β π) |
90 | 59, 89 | eqeltrd 2838 |
. 2
β’ ((π β LMod β§ (π β π β§ π β LMod)) β π β π) |
91 | 57, 90 | impbida 800 |
1
β’ (π β LMod β (π β π β (π β π β§ π β LMod))) |