# Metamath Proof Explorer

## Theorem islininds2

Description: Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps2.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
islindeps2.z ${⊢}{Z}={0}_{{M}}$
islindeps2.r ${⊢}{R}=\mathrm{Scalar}\left({M}\right)$
islindeps2.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
islindeps2.0
Assertion islininds2

### Proof

Step Hyp Ref Expression
1 islindeps2.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 islindeps2.z ${⊢}{Z}={0}_{{M}}$
3 islindeps2.r ${⊢}{R}=\mathrm{Scalar}\left({M}\right)$
4 islindeps2.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
5 islindeps2.0
6 lindepsnlininds ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\right)\to \left({S}\mathrm{linDepS}{M}↔¬{S}\mathrm{linIndS}{M}\right)$
7 6 ancoms ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\right)\to \left({S}\mathrm{linDepS}{M}↔¬{S}\mathrm{linIndS}{M}\right)$
8 7 3adant3 ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\to \left({S}\mathrm{linDepS}{M}↔¬{S}\mathrm{linIndS}{M}\right)$
9 8 con2bid ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\to \left({S}\mathrm{linIndS}{M}↔¬{S}\mathrm{linDepS}{M}\right)$
10 notnotb
11 nne ${⊢}¬{f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)\ne {s}↔{f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}$
12 11 bicomi ${⊢}{f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}↔¬{f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)\ne {s}$
13 10 12 anbi12i
14 pm4.56
15 13 14 bitri
16 15 rexbii
17 rexnal
18 16 17 bitri
19 18 rexbii
20 rexnal
21 19 20 bitri
22 1 2 3 4 5 islindeps2
23 21 22 syl5bir
24 23 con1d
25 9 24 sylbid