Metamath Proof Explorer


Theorem el0ldepsnzr

Description: A set containing the zero element of a module over a nonzero ring is always linearly dependent. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

Ref Expression
Assertion el0ldepsnzr MLModScalarMNzRingS𝒫BaseM0MSSlinDepSM

Proof

Step Hyp Ref Expression
1 simp1l MLModScalarMNzRingS𝒫BaseM0MSMLMod
2 eqid BaseScalarM=BaseScalarM
3 2 isnzr2hash ScalarMNzRingScalarMRing1<BaseScalarM
4 3 simprbi ScalarMNzRing1<BaseScalarM
5 4 adantl MLModScalarMNzRing1<BaseScalarM
6 5 3ad2ant1 MLModScalarMNzRingS𝒫BaseM0MS1<BaseScalarM
7 1 6 jca MLModScalarMNzRingS𝒫BaseM0MSMLMod1<BaseScalarM
8 el0ldep MLMod1<BaseScalarMS𝒫BaseM0MSSlinDepSM
9 7 8 syld3an1 MLModScalarMNzRingS𝒫BaseM0MSSlinDepSM