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 ‘ 𝑀 ) } )