Metamath Proof Explorer


Theorem lindslininds

Description: Equivalence of definitions df-linds and df-lininds for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion lindslininds S V M LMod S linIndS M S LIndS M

Proof

Step Hyp Ref Expression
1 eqid Scalar M = Scalar M
2 eqid Base Scalar M = Base Scalar M
3 eqid 0 Scalar M = 0 Scalar M
4 eqid 0 M = 0 M
5 1 2 3 4 lindslinindsimp1 S V M LMod S 𝒫 Base M f Base Scalar M S finSupp 0 Scalar M f f linC M S = 0 M x S f x = 0 Scalar M S Base M s S g Base Scalar M 0 Scalar M ¬ g M s LSpan M S s
6 1 2 3 4 lindslinindsimp2 S V M LMod S Base M s S g Base Scalar M 0 Scalar M ¬ g M s LSpan M S s S 𝒫 Base M f Base Scalar M S finSupp 0 Scalar M f f linC M S = 0 M x S f x = 0 Scalar M
7 5 6 impbid S V M LMod S 𝒫 Base M f Base Scalar M S finSupp 0 Scalar M f f linC M S = 0 M x S f x = 0 Scalar M S Base M s S g Base Scalar M 0 Scalar M ¬ g M s LSpan M S s
8 eqid Base M = Base M
9 8 4 1 2 3 islininds S V M LMod S linIndS M S 𝒫 Base M f Base Scalar M S finSupp 0 Scalar M f f linC M S = 0 M x S f x = 0 Scalar M
10 eqid M = M
11 eqid LSpan M = LSpan M
12 8 10 11 1 2 3 islinds2 M LMod S LIndS M S Base M s S g Base Scalar M 0 Scalar M ¬ g M s LSpan M S s
13 12 adantl S V M LMod S LIndS M S Base M s S g Base Scalar M 0 Scalar M ¬ g M s LSpan M S s
14 7 9 13 3bitr4d S V M LMod S linIndS M S LIndS M