# Metamath Proof Explorer

## Theorem islindeps2

Description: Conditions for being a linearly dependent 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 islindeps2

### 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 id ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\right)\to \left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\right)$
7 6 3adant3 ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\to \left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\right)$
9 nzrring ${⊢}{R}\in \mathrm{NzRing}\to {R}\in \mathrm{Ring}$
10 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
11 4 10 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {E}$
12 9 11 syl ${⊢}{R}\in \mathrm{NzRing}\to {1}_{{R}}\in {E}$
13 12 3ad2ant3 ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\to {1}_{{R}}\in {E}$
15 simpllr
16 simplr
17 14 15 16 3jca
18 simprl
19 eqid ${⊢}{inv}_{g}\left({R}\right)={inv}_{g}\left({R}\right)$
20 eqid ${⊢}\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)$
21 1 3 4 5 2 19 20 lincext2
22 8 17 18 21 syl3anc
23 simpl1 ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to {M}\in \mathrm{LMod}$
24 elelpwi ${⊢}\left({s}\in {S}\wedge {S}\in 𝒫{B}\right)\to {s}\in {B}$
25 24 expcom ${⊢}{S}\in 𝒫{B}\to \left({s}\in {S}\to {s}\in {B}\right)$
26 25 3ad2ant2 ${⊢}\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\to \left({s}\in {S}\to {s}\in {B}\right)$
27 26 imp ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to {s}\in {B}$
28 eqid ${⊢}{\cdot }_{{M}}={\cdot }_{{M}}$
29 1 3 28 10 lmodvs1 ${⊢}\left({M}\in \mathrm{LMod}\wedge {s}\in {B}\right)\to {1}_{{R}}{\cdot }_{{M}}{s}={s}$
30 23 27 29 syl2anc ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to {1}_{{R}}{\cdot }_{{M}}{s}={s}$
31 30 adantr ${⊢}\left(\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\wedge {f}\in \left({{E}}^{\left({S}\setminus \left\{{s}\right\}\right)}\right)\right)\to {1}_{{R}}{\cdot }_{{M}}{s}={s}$
32 id ${⊢}{f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}\to {f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}$
33 32 eqcomd ${⊢}{f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}\to {s}={f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)$
35 31 34 sylan9eq
36 1 3 4 5 2 19 20 lincext3
37 8 17 18 35 36 syl112anc
38 22 37 jca
39 eqidd ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to \left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)$
40 iftrue ${⊢}{z}={s}\to if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)={inv}_{g}\left({R}\right)\left({1}_{{R}}\right)$
41 40 adantl ${⊢}\left(\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\wedge {z}={s}\right)\to if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)={inv}_{g}\left({R}\right)\left({1}_{{R}}\right)$
42 simpr ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to {s}\in {S}$
43 fvexd ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to {inv}_{g}\left({R}\right)\left({1}_{{R}}\right)\in \mathrm{V}$
44 39 41 42 43 fvmptd ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\wedge {R}\in \mathrm{NzRing}\right)\wedge {s}\in {S}\right)\to \left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\left({s}\right)={inv}_{g}\left({R}\right)\left({1}_{{R}}\right)$
45 nzrneg1ne0 ${⊢}{R}\in \mathrm{NzRing}\to {inv}_{g}\left({R}\right)\left({1}_{{R}}\right)\ne {0}_{{R}}$
46 5 a1i
47 45 46 neeqtrrd
50 44 49 eqnetrd
53 1 3 4 5 2 19 20 lincext1 ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\in 𝒫{B}\right)\wedge \left({1}_{{R}}\in {E}\wedge {s}\in {S}\wedge {f}\in \left({{E}}^{\left({S}\setminus \left\{{s}\right\}\right)}\right)\right)\right)\to \left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\in \left({{E}}^{{S}}\right)$
54 8 17 53 syl2anc
55 breq1
56 oveq1 ${⊢}{g}=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\to {g}\mathrm{linC}\left({M}\right){S}=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\mathrm{linC}\left({M}\right){S}$
57 56 eqeq1d ${⊢}{g}=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\to \left({g}\mathrm{linC}\left({M}\right){S}={Z}↔\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\mathrm{linC}\left({M}\right){S}={Z}\right)$
58 55 57 anbi12d
59 fveq1 ${⊢}{g}=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\to {g}\left({s}\right)=\left({z}\in {S}⟼if\left({z}={s},{inv}_{g}\left({R}\right)\left({1}_{{R}}\right),{f}\left({z}\right)\right)\right)\left({s}\right)$
60 59 neeq1d
61 58 60 anbi12d
63 54 62 rspcedv
64 38 52 63 mp2and
65 64 rexlimdva2
66 65 reximdva
67 66 imp
68 df-3an
69 r19.42v
70 68 69 bitr4i
71 70 rexbii
72 rexcom
73 71 72 bitri
74 67 73 sylibr
75 1 2 3 4 5 islindeps