Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β π β LMod) |
2 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
3 | | lssvsubcl.s |
. . . . 5
β’ π = (LSubSpβπ) |
4 | 2, 3 | lssel 20413 |
. . . 4
β’ ((π β π β§ π β π) β π β (Baseβπ)) |
5 | 4 | ad2ant2lr 747 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β π β (Baseβπ)) |
6 | 2, 3 | lssel 20413 |
. . . 4
β’ ((π β π β§ π β π) β π β (Baseβπ)) |
7 | 6 | ad2ant2l 745 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β π β (Baseβπ)) |
8 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
9 | | lssvsubcl.m |
. . . 4
β’ β =
(-gβπ) |
10 | | eqid 2733 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
11 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
12 | | eqid 2733 |
. . . 4
β’
(invgβ(Scalarβπ)) =
(invgβ(Scalarβπ)) |
13 | | eqid 2733 |
. . . 4
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
14 | 2, 8, 9, 10, 11, 12, 13 | lmodvsubval2 20392 |
. . 3
β’ ((π β LMod β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π β π) = (π(+gβπ)(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π))) |
15 | 1, 5, 7, 14 | syl3anc 1372 |
. 2
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π β π) = (π(+gβπ)(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π))) |
16 | 10 | lmodfgrp 20345 |
. . . . . . 7
β’ (π β LMod β
(Scalarβπ) β
Grp) |
17 | 1, 16 | syl 17 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (Scalarβπ) β Grp) |
18 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
19 | 10, 18, 13 | lmod1cl 20364 |
. . . . . . 7
β’ (π β LMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
20 | 1, 19 | syl 17 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
21 | 18, 12 | grpinvcl 18803 |
. . . . . 6
β’
(((Scalarβπ)
β Grp β§ (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
22 | 17, 20, 21 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
23 | 2, 10, 11, 18 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))
β§ π β (Baseβπ)) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π) β (Baseβπ)) |
24 | 1, 22, 7, 23 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π) β (Baseβπ)) |
25 | 2, 8 | lmodcom 20383 |
. . . 4
β’ ((π β LMod β§ π β (Baseβπ) β§
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π) β (Baseβπ)) β (π(+gβπ)(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)) =
((((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)(+gβπ)π)) |
26 | 1, 5, 24, 25 | syl3anc 1372 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π(+gβπ)(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)) =
((((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)(+gβπ)π)) |
27 | | simplr 768 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β π β π) |
28 | | simprr 772 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β π β π) |
29 | | simprl 770 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β π β π) |
30 | 10, 18, 8, 11, 3 | lsscl 20418 |
. . . 4
β’ ((π β π β§
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))
β§ π β π β§ π β π)) β
((((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)(+gβπ)π) β π) |
31 | 27, 22, 28, 29, 30 | syl13anc 1373 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β
((((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)(+gβπ)π) β π) |
32 | 26, 31 | eqeltrd 2834 |
. 2
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π(+gβπ)(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)) β π) |
33 | 15, 32 | eqeltrd 2834 |
1
β’ (((π β LMod β§ π β π) β§ (π β π β§ π β π)) β (π β π) β π) |