Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
2 | 1 | lmodring 20346 |
. . 3
β’ (π β LMod β
(Scalarβπ) β
Ring) |
3 | | 0ringnnzr 20755 |
. . . . 5
β’
((Scalarβπ)
β Ring β ((β―β(Baseβ(Scalarβπ))) = 1 β Β¬ (Scalarβπ) β
NzRing)) |
4 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
5 | | eqid 2737 |
. . . . . . . 8
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
6 | | eqid 2737 |
. . . . . . . 8
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
7 | 4, 5, 6 | 0ring01eq 20757 |
. . . . . . 7
β’
(((Scalarβπ)
β Ring β§ (β―β(Baseβ(Scalarβπ))) = 1) β
(0gβ(Scalarβπ)) =
(1rβ(Scalarβπ))) |
8 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
9 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (
Β·π βπ) = ( Β·π
βπ) |
10 | 8, 1, 9, 6 | lmodvs1 20366 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π£ β (Baseβπ)) β
((1rβ(Scalarβπ))( Β·π
βπ)π£) = π£) |
11 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
β’
(((1rβ(Scalarβπ))( Β·π
βπ)π£) = π£ β π£ = ((1rβ(Scalarβπ))(
Β·π βπ)π£)) |
12 | 11 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’
(((1rβ(Scalarβπ))( Β·π
βπ)π£) = π£ β π£ = ((1rβ(Scalarβπ))(
Β·π βπ)π£)) |
13 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’
((1rβ(Scalarβπ)) =
(0gβ(Scalarβπ)) β
((1rβ(Scalarβπ))( Β·π
βπ)π£) = ((0gβ(Scalarβπ))(
Β·π βπ)π£)) |
14 | 13 | eqcoms 2745 |
. . . . . . . . . . . . . . . 16
β’
((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β
((1rβ(Scalarβπ))( Β·π
βπ)π£) = ((0gβ(Scalarβπ))(
Β·π βπ)π£)) |
15 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(0gβπ) = (0gβπ) |
16 | 8, 1, 9, 5, 15 | lmod0vs 20371 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π£ β (Baseβπ)) β
((0gβ(Scalarβπ))( Β·π
βπ)π£) = (0gβπ)) |
17 | 14, 16 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
β’ (((π β LMod β§ π£ β (Baseβπ)) β§
(0gβ(Scalarβπ)) =
(1rβ(Scalarβπ))) β
((1rβ(Scalarβπ))( Β·π
βπ)π£) = (0gβπ)) |
18 | 12, 17 | sylan9eq 2797 |
. . . . . . . . . . . . . 14
β’
((((1rβ(Scalarβπ))( Β·π
βπ)π£) = π£ β§ ((π β LMod β§ π£ β (Baseβπ)) β§
(0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)))) β π£ = (0gβπ)) |
19 | 18 | exp32 422 |
. . . . . . . . . . . . 13
β’
(((1rβ(Scalarβπ))( Β·π
βπ)π£) = π£ β ((π β LMod β§ π£ β (Baseβπ)) β
((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β π£ = (0gβπ)))) |
20 | 10, 19 | mpcom 38 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π£ β (Baseβπ)) β
((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β π£ = (0gβπ))) |
21 | 20 | com12 32 |
. . . . . . . . . . 11
β’
((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β ((π β LMod β§ π£ β (Baseβπ)) β π£ = (0gβπ))) |
22 | 21 | impl 457 |
. . . . . . . . . 10
β’
((((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β§ π β LMod) β§ π£ β (Baseβπ)) β π£ = (0gβπ)) |
23 | 22 | ralrimiva 3144 |
. . . . . . . . 9
β’
(((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β§ π β LMod) β βπ£ β (Baseβπ)π£ = (0gβπ)) |
24 | 8 | lmodbn0 20348 |
. . . . . . . . . . 11
β’ (π β LMod β
(Baseβπ) β
β
) |
25 | | eqsn 4794 |
. . . . . . . . . . 11
β’
((Baseβπ) β
β
β ((Baseβπ) = {(0gβπ)} β βπ£ β (Baseβπ)π£ = (0gβπ))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ (π β LMod β
((Baseβπ) =
{(0gβπ)}
β βπ£ β
(Baseβπ)π£ = (0gβπ))) |
27 | 26 | adantl 483 |
. . . . . . . . 9
β’
(((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β§ π β LMod) β ((Baseβπ) = {(0gβπ)} β βπ£ β (Baseβπ)π£ = (0gβπ))) |
28 | 23, 27 | mpbird 257 |
. . . . . . . 8
β’
(((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β§ π β LMod) β (Baseβπ) = {(0gβπ)}) |
29 | 28 | ex 414 |
. . . . . . 7
β’
((0gβ(Scalarβπ)) =
(1rβ(Scalarβπ)) β (π β LMod β (Baseβπ) = {(0gβπ)})) |
30 | 7, 29 | syl 17 |
. . . . . 6
β’
(((Scalarβπ)
β Ring β§ (β―β(Baseβ(Scalarβπ))) = 1) β (π β LMod β (Baseβπ) = {(0gβπ)})) |
31 | 30 | ex 414 |
. . . . 5
β’
((Scalarβπ)
β Ring β ((β―β(Baseβ(Scalarβπ))) = 1 β (π β LMod β (Baseβπ) = {(0gβπ)}))) |
32 | 3, 31 | sylbird 260 |
. . . 4
β’
((Scalarβπ)
β Ring β (Β¬ (Scalarβπ) β NzRing β (π β LMod β (Baseβπ) = {(0gβπ)}))) |
33 | 32 | com23 86 |
. . 3
β’
((Scalarβπ)
β Ring β (π
β LMod β (Β¬ (Scalarβπ) β NzRing β (Baseβπ) = {(0gβπ)}))) |
34 | 2, 33 | mpcom 38 |
. 2
β’ (π β LMod β (Β¬
(Scalarβπ) β
NzRing β (Baseβπ) = {(0gβπ)})) |
35 | 34 | imp 408 |
1
β’ ((π β LMod β§ Β¬
(Scalarβπ) β
NzRing) β (Baseβπ) = {(0gβπ)}) |