Metamath Proof Explorer

Theorem lmod0rng

Description: If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019)

Ref Expression
Assertion lmod0rng ⊢M∈LMod∧¬Scalar⁡M∈NzRing→BaseM=0M

Proof

Step Hyp Ref Expression
1 eqid ⊢Scalar⁡M=Scalar⁡M
2 1 lmodring ⊢M∈LMod→Scalar⁡M∈Ring
3 0ringnnzr ⊢Scalar⁡M∈Ring→BaseScalar⁡M=1↔¬Scalar⁡M∈NzRing
4 eqid ⊢BaseScalar⁡M=BaseScalar⁡M
5 eqid ⊢0Scalar⁡M=0Scalar⁡M
6 eqid ⊢1Scalar⁡M=1Scalar⁡M
7 4 5 6 0ring01eq ⊢Scalar⁡M∈Ring∧BaseScalar⁡M=1→0Scalar⁡M=1Scalar⁡M
8 eqid ⊢BaseM=BaseM
9 eqid ⊢⋅M=⋅M
10 8 1 9 6 lmodvs1 ⊢M∈LMod∧v∈BaseM→1Scalar⁡M⋅Mv=v
11 eqcom ⊢1Scalar⁡M⋅Mv=v↔v=1Scalar⁡M⋅Mv
12 11 biimpi ⊢1Scalar⁡M⋅Mv=v→v=1Scalar⁡M⋅Mv
13 oveq1 ⊢1Scalar⁡M=0Scalar⁡M→1Scalar⁡M⋅Mv=0Scalar⁡M⋅Mv
14 13 eqcoms ⊢0Scalar⁡M=1Scalar⁡M→1Scalar⁡M⋅Mv=0Scalar⁡M⋅Mv
15 eqid ⊢0M=0M
16 8 1 9 5 15 lmod0vs ⊢M∈LMod∧v∈BaseM→0Scalar⁡M⋅Mv=0M
17 14 16 sylan9eqr ⊢M∈LMod∧v∈BaseM∧0Scalar⁡M=1Scalar⁡M→1Scalar⁡M⋅Mv=0M
18 12 17 sylan9eq ⊢1Scalar⁡M⋅Mv=v∧M∈LMod∧v∈BaseM∧0Scalar⁡M=1Scalar⁡M→v=0M
19 18 exp32 ⊢1Scalar⁡M⋅Mv=v→M∈LMod∧v∈BaseM→0Scalar⁡M=1Scalar⁡M→v=0M
20 10 19 mpcom ⊢M∈LMod∧v∈BaseM→0Scalar⁡M=1Scalar⁡M→v=0M
21 20 com12 ⊢0Scalar⁡M=1Scalar⁡M→M∈LMod∧v∈BaseM→v=0M
22 21 impl ⊢0Scalar⁡M=1Scalar⁡M∧M∈LMod∧v∈BaseM→v=0M
23 22 ralrimiva ⊢0Scalar⁡M=1Scalar⁡M∧M∈LMod→∀v∈BaseMv=0M
24 8 lmodbn0 ⊢M∈LMod→BaseM≠∅
25 eqsn ⊢BaseM≠∅→BaseM=0M↔∀v∈BaseMv=0M
26 24 25 syl ⊢M∈LMod→BaseM=0M↔∀v∈BaseMv=0M
27 26 adantl ⊢0Scalar⁡M=1Scalar⁡M∧M∈LMod→BaseM=0M↔∀v∈BaseMv=0M
28 23 27 mpbird ⊢0Scalar⁡M=1Scalar⁡M∧M∈LMod→BaseM=0M
29 28 ex ⊢0Scalar⁡M=1Scalar⁡M→M∈LMod→BaseM=0M
30 7 29 syl ⊢Scalar⁡M∈Ring∧BaseScalar⁡M=1→M∈LMod→BaseM=0M
31 30 ex ⊢Scalar⁡M∈Ring→BaseScalar⁡M=1→M∈LMod→BaseM=0M
32 3 31 sylbird ⊢Scalar⁡M∈Ring→¬Scalar⁡M∈NzRing→M∈LMod→BaseM=0M
33 32 com23 ⊢Scalar⁡M∈Ring→M∈LMod→¬Scalar⁡M∈NzRing→BaseM=0M
34 2 33 mpcom ⊢M∈LMod→¬Scalar⁡M∈NzRing→BaseM=0M
35 34 imp ⊢M∈LMod∧¬Scalar⁡M∈NzRing→BaseM=0M