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 ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ) → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
2 1 lmodring ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Ring )
3 0ringnnzr ⊢ ( ( Scalar ‘ 𝑀 ) ∈ Ring → ( ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ↔ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ) )
4 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
5 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
6 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) )
7 4 5 6 0ring01eq ⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ) → ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) )
8 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
9 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
10 8 1 9 6 lmodvs1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑣 )
11 eqcom ⊢ ( ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑣 ↔ 𝑣 = ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
12 11 biimpi ⊢ ( ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑣 → 𝑣 = ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
13 oveq1 ⊢ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
14 13 eqcoms ⊢ ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
15 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
16 8 1 9 5 15 lmod0vs ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0g ‘ 𝑀 ) )
17 14 16 sylan9eqr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) ∧ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0g ‘ 𝑀 ) )
18 12 17 sylan9eq ⊢ ( ( ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑣 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) ∧ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ) ) → 𝑣 = ( 0g ‘ 𝑀 ) )
19 18 exp32 ⊢ ( ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑣 → ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) → 𝑣 = ( 0g ‘ 𝑀 ) ) ) )
20 10 19 mpcom ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) → 𝑣 = ( 0g ‘ 𝑀 ) ) )
21 20 com12 ⊢ ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → 𝑣 = ( 0g ‘ 𝑀 ) ) )
22 21 impl ⊢ ( ( ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑀 ∈ LMod ) ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → 𝑣 = ( 0g ‘ 𝑀 ) )
23 22 ralrimiva ⊢ ( ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑀 ∈ LMod ) → ∀ 𝑣 ∈ ( Base ‘ 𝑀 ) 𝑣 = ( 0g ‘ 𝑀 ) )
24 8 lmodbn0 ⊢ ( 𝑀 ∈ LMod → ( Base ‘ 𝑀 ) ≠ ∅ )
25 eqsn ⊢ ( ( Base ‘ 𝑀 ) ≠ ∅ → ( ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑀 ) 𝑣 = ( 0g ‘ 𝑀 ) ) )
26 24 25 syl ⊢ ( 𝑀 ∈ LMod → ( ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑀 ) 𝑣 = ( 0g ‘ 𝑀 ) ) )
27 26 adantl ⊢ ( ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑀 ∈ LMod ) → ( ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑀 ) 𝑣 = ( 0g ‘ 𝑀 ) ) )
28 23 27 mpbird ⊢ ( ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑀 ∈ LMod ) → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } )
29 28 ex ⊢ ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) → ( 𝑀 ∈ LMod → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ) )
30 7 29 syl ⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ) → ( 𝑀 ∈ LMod → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ) )
31 30 ex ⊢ ( ( Scalar ‘ 𝑀 ) ∈ Ring → ( ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 → ( 𝑀 ∈ LMod → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ) ) )
32 3 31 sylbird ⊢ ( ( Scalar ‘ 𝑀 ) ∈ Ring → ( ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing → ( 𝑀 ∈ LMod → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ) ) )
33 32 com23 ⊢ ( ( Scalar ‘ 𝑀 ) ∈ Ring → ( 𝑀 ∈ LMod → ( ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ) ) )
34 2 33 mpcom ⊢ ( 𝑀 ∈ LMod → ( ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } ) )
35 34 imp ⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ) → ( Base ‘ 𝑀 ) = { ( 0g ‘ 𝑀 ) } )