Theorem lindszr

Description: Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019)

	Ref	Expression
Assertion	lindszr	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑆 linIndS 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing )
2		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
3	2	lmodring	⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Ring )
4	3	3ad2ant1	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
5		0ringnnzr	⊢ ( ( Scalar ‘ 𝑀 ) ∈ Ring → ( ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ↔ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ) )
6	4 5	syl	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ↔ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ) )
7	1 6	mpbird	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 )
8	7	olcd	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 0 ∨ ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ) )
9		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
10		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
11	9 2 10	lindsrng01	⊢ ( ( 𝑀 ∈ LMod ∧ ( ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 0 ∨ ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) = 1 ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑆 linIndS 𝑀 )
12	8 11	syld3an2	⊢ ( ( 𝑀 ∈ LMod ∧ ¬ ( Scalar ‘ 𝑀 ) ∈ NzRing ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑆 linIndS 𝑀 )