Step | Hyp | Ref
| Expression |
1 | | slmdvs0.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
2 | 1 | slmdsrg 32352 |
. . . 4
β’ (π β SLMod β πΉ β SRing) |
3 | | slmdvs0.k |
. . . . 5
β’ πΎ = (BaseβπΉ) |
4 | | eqid 2733 |
. . . . 5
β’
(.rβπΉ) = (.rβπΉ) |
5 | | eqid 2733 |
. . . . 5
β’
(0gβπΉ) = (0gβπΉ) |
6 | 3, 4, 5 | srgrz 20030 |
. . . 4
β’ ((πΉ β SRing β§ π β πΎ) β (π(.rβπΉ)(0gβπΉ)) = (0gβπΉ)) |
7 | 2, 6 | sylan 581 |
. . 3
β’ ((π β SLMod β§ π β πΎ) β (π(.rβπΉ)(0gβπΉ)) = (0gβπΉ)) |
8 | 7 | oveq1d 7424 |
. 2
β’ ((π β SLMod β§ π β πΎ) β ((π(.rβπΉ)(0gβπΉ)) Β· 0 ) =
((0gβπΉ)
Β·
0
)) |
9 | | simpl 484 |
. . . 4
β’ ((π β SLMod β§ π β πΎ) β π β SLMod) |
10 | | simpr 486 |
. . . 4
β’ ((π β SLMod β§ π β πΎ) β π β πΎ) |
11 | 2 | adantr 482 |
. . . . 5
β’ ((π β SLMod β§ π β πΎ) β πΉ β SRing) |
12 | 3, 5 | srg0cl 20023 |
. . . . 5
β’ (πΉ β SRing β
(0gβπΉ)
β πΎ) |
13 | 11, 12 | syl 17 |
. . . 4
β’ ((π β SLMod β§ π β πΎ) β (0gβπΉ) β πΎ) |
14 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
15 | | slmdvs0.z |
. . . . . 6
β’ 0 =
(0gβπ) |
16 | 14, 15 | slmd0vcl 32366 |
. . . . 5
β’ (π β SLMod β 0 β
(Baseβπ)) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π β SLMod β§ π β πΎ) β 0 β (Baseβπ)) |
18 | | slmdvs0.s |
. . . . 5
β’ Β· = (
Β·π βπ) |
19 | 14, 1, 18, 3, 4 | slmdvsass 32362 |
. . . 4
β’ ((π β SLMod β§ (π β πΎ β§ (0gβπΉ) β πΎ β§ 0 β (Baseβπ))) β ((π(.rβπΉ)(0gβπΉ)) Β· 0 ) = (π Β·
((0gβπΉ)
Β·
0
))) |
20 | 9, 10, 13, 17, 19 | syl13anc 1373 |
. . 3
β’ ((π β SLMod β§ π β πΎ) β ((π(.rβπΉ)(0gβπΉ)) Β· 0 ) = (π Β·
((0gβπΉ)
Β·
0
))) |
21 | 14, 1, 18, 5, 15 | slmd0vs 32369 |
. . . . 5
β’ ((π β SLMod β§ 0 β
(Baseβπ)) β
((0gβπΉ)
Β·
0 ) =
0
) |
22 | 17, 21 | syldan 592 |
. . . 4
β’ ((π β SLMod β§ π β πΎ) β ((0gβπΉ) Β· 0 ) = 0 ) |
23 | 22 | oveq2d 7425 |
. . 3
β’ ((π β SLMod β§ π β πΎ) β (π Β·
((0gβπΉ)
Β·
0 )) =
(π Β· 0 )) |
24 | 20, 23 | eqtrd 2773 |
. 2
β’ ((π β SLMod β§ π β πΎ) β ((π(.rβπΉ)(0gβπΉ)) Β· 0 ) = (π Β· 0 )) |
25 | 8, 24, 22 | 3eqtr3d 2781 |
1
β’ ((π β SLMod β§ π β πΎ) β (π Β· 0 ) = 0 ) |