Step | Hyp | Ref
| Expression |
1 | | lmodabl 20384 |
. . . 4
β’ (π β LMod β π β Abel) |
2 | 1 | 3ad2ant1 1134 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β π β Abel) |
3 | | lsmcl.s |
. . . . 5
β’ π = (LSubSpβπ) |
4 | 3 | lsssubg 20433 |
. . . 4
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
5 | 4 | 3adant3 1133 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β π β (SubGrpβπ)) |
6 | 3 | lsssubg 20433 |
. . . 4
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
7 | 6 | 3adant2 1132 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β π β (SubGrpβπ)) |
8 | | lsmcl.p |
. . . 4
β’ β =
(LSSumβπ) |
9 | 8 | lsmsubg2 19642 |
. . 3
β’ ((π β Abel β§ π β (SubGrpβπ) β§ π β (SubGrpβπ)) β (π β π) β (SubGrpβπ)) |
10 | 2, 5, 7, 9 | syl3anc 1372 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β (SubGrpβπ)) |
11 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
12 | 11, 8 | lsmelval 19436 |
. . . . . . 7
β’ ((π β (SubGrpβπ) β§ π β (SubGrpβπ)) β (π’ β (π β π) β βπ β π βπ β π π’ = (π(+gβπ)π))) |
13 | 5, 7, 12 | syl2anc 585 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π’ β (π β π) β βπ β π βπ β π π’ = (π(+gβπ)π))) |
14 | 13 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β (π’ β (π β π) β βπ β π βπ β π π’ = (π(+gβπ)π))) |
15 | | simpll1 1213 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β LMod) |
16 | | simplr 768 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β (Baseβ(Scalarβπ))) |
17 | | simpll2 1214 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β π) |
18 | | simprl 770 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β π) |
19 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
20 | 19, 3 | lssel 20413 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β π β (Baseβπ)) |
21 | 17, 18, 20 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β (Baseβπ)) |
22 | | simpll3 1215 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β π) |
23 | | simprr 772 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β π) |
24 | 19, 3 | lssel 20413 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β π β (Baseβπ)) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β (Baseβπ)) |
26 | | eqid 2733 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
27 | | eqid 2733 |
. . . . . . . . . 10
β’ (
Β·π βπ) = ( Β·π
βπ) |
28 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
29 | 19, 11, 26, 27, 28 | lmodvsdi 20360 |
. . . . . . . . 9
β’ ((π β LMod β§ (π β
(Baseβ(Scalarβπ)) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)(π(+gβπ)π)) = ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π))) |
30 | 15, 16, 21, 25, 29 | syl13anc 1373 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β (π( Β·π
βπ)(π(+gβπ)π)) = ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π))) |
31 | 15, 17, 4 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β (SubGrpβπ)) |
32 | 15, 22, 6 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β π β (SubGrpβπ)) |
33 | 26, 27, 28, 3 | lssvscl 20431 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)π) β π) |
34 | 15, 17, 16, 18, 33 | syl22anc 838 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β (π( Β·π
βπ)π) β π) |
35 | 26, 27, 28, 3 | lssvscl 20431 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)π) β π) |
36 | 15, 22, 16, 23, 35 | syl22anc 838 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β (π( Β·π
βπ)π) β π) |
37 | 11, 8 | lsmelvali 19437 |
. . . . . . . . 9
β’ (((π β (SubGrpβπ) β§ π β (SubGrpβπ)) β§ ((π( Β·π
βπ)π) β π β§ (π( Β·π
βπ)π) β π)) β ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π)) β (π β π)) |
38 | 31, 32, 34, 36, 37 | syl22anc 838 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π)) β (π β π)) |
39 | 30, 38 | eqeltrd 2834 |
. . . . . . 7
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β (π( Β·π
βπ)(π(+gβπ)π)) β (π β π)) |
40 | | oveq2 7366 |
. . . . . . . 8
β’ (π’ = (π(+gβπ)π) β (π( Β·π
βπ)π’) = (π( Β·π
βπ)(π(+gβπ)π))) |
41 | 40 | eleq1d 2819 |
. . . . . . 7
β’ (π’ = (π(+gβπ)π) β ((π( Β·π
βπ)π’) β (π β π) β (π( Β·π
βπ)(π(+gβπ)π)) β (π β π))) |
42 | 39, 41 | syl5ibrcom 247 |
. . . . . 6
β’ ((((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ (π β π β§ π β π)) β (π’ = (π(+gβπ)π) β (π( Β·π
βπ)π’) β (π β π))) |
43 | 42 | rexlimdvva 3202 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β (βπ β π βπ β π π’ = (π(+gβπ)π) β (π( Β·π
βπ)π’) β (π β π))) |
44 | 14, 43 | sylbid 239 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β (π’ β (π β π) β (π( Β·π
βπ)π’) β (π β π))) |
45 | 44 | impr 456 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π’ β (π β π))) β (π( Β·π
βπ)π’) β (π β π)) |
46 | 45 | ralrimivva 3194 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β βπ β (Baseβ(Scalarβπ))βπ’ β (π β π)(π( Β·π
βπ)π’) β (π β π)) |
47 | 26, 28, 19, 27, 3 | islss4 20438 |
. . 3
β’ (π β LMod β ((π β π) β π β ((π β π) β (SubGrpβπ) β§ βπ β (Baseβ(Scalarβπ))βπ’ β (π β π)(π( Β·π
βπ)π’) β (π β π)))) |
48 | 47 | 3ad2ant1 1134 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β ((π β π) β π β ((π β π) β (SubGrpβπ) β§ βπ β (Baseβ(Scalarβπ))βπ’ β (π β π)(π( Β·π
βπ)π’) β (π β π)))) |
49 | 10, 46, 48 | mpbir2and 712 |
1
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |