# Metamath Proof Explorer

## Theorem isldepslvec2

Description: Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 holds, so that both definitions are equivalent (see theorem 1.6 in Roman p. 46 and the note in Roman p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-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 isldepslvec2

### 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 lveclmod ${⊢}{M}\in \mathrm{LVec}\to {M}\in \mathrm{LMod}$
7 6 adantr ${⊢}\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\to {M}\in \mathrm{LMod}$
8 simpr ${⊢}\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\to {S}\in 𝒫{B}$
9 3 lvecdrng ${⊢}{M}\in \mathrm{LVec}\to {R}\in \mathrm{DivRing}$
10 drngnzr ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{NzRing}$
11 9 10 syl ${⊢}{M}\in \mathrm{LVec}\to {R}\in \mathrm{NzRing}$
12 11 adantr ${⊢}\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\to {R}\in \mathrm{NzRing}$
13 1 2 3 4 5 islindeps2
14 7 8 12 13 syl3anc
15 1 2 3 4 5 islindeps
16 df-3an
17 r19.42v
18 16 17 bitr4i
19 18 rexbii
20 rexcom
21 19 20 bitri
22 simplr ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to {S}\in 𝒫{B}$
23 6 ad2antrr ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to {M}\in \mathrm{LMod}$
24 simpr ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to {s}\in {S}$
25 22 23 24 3jca ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {s}\in {S}\right)$
27 simplr
28 elmapi ${⊢}{g}\in \left({{E}}^{{S}}\right)\to {g}:{S}⟶{E}$
29 ffvelrn ${⊢}\left({g}:{S}⟶{E}\wedge {s}\in {S}\right)\to {g}\left({s}\right)\in {E}$
30 28 24 29 syl2anr ${⊢}\left(\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\wedge {g}\in \left({{E}}^{{S}}\right)\right)\to {g}\left({s}\right)\in {E}$
31 simpr
32 30 31 anim12i
33 9 ad2antrr ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to {R}\in \mathrm{DivRing}$
35 eqid ${⊢}\mathrm{Unit}\left({R}\right)=\mathrm{Unit}\left({R}\right)$
36 4 35 5 drngunit
37 34 36 syl
38 32 37 mpbird
39 simpll
41 eqid ${⊢}{inv}_{g}\left({R}\right)={inv}_{g}\left({R}\right)$
42 eqid ${⊢}{inv}_{r}\left({R}\right)={inv}_{r}\left({R}\right)$
43 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
44 eqid ${⊢}\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)=\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)$
45 1 3 4 35 5 2 41 42 43 44 lincresunit2
46 26 27 38 40 45 syl13anc
47 simpll ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to {M}\in \mathrm{LVec}$
48 22 47 24 3jca ${⊢}\left(\left({M}\in \mathrm{LVec}\wedge {S}\in 𝒫{B}\right)\wedge {s}\in {S}\right)\to \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LVec}\wedge {s}\in {S}\right)$
50 simprr
51 simplr
53 fveq2 ${⊢}{z}={y}\to {g}\left({z}\right)={g}\left({y}\right)$
54 53 oveq2d ${⊢}{z}={y}\to {inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)={inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({y}\right)$
55 54 cbvmptv ${⊢}\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)=\left({y}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({y}\right)\right)$
56 1 3 4 35 5 2 41 42 43 55 lincreslvec3
57 49 27 50 40 52 56 syl131anc
58 1 3 4 35 5 2 41 42 43 44 lincresunit1 ${⊢}\left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {s}\in {S}\right)\wedge \left({g}\in \left({{E}}^{{S}}\right)\wedge {g}\left({s}\right)\in \mathrm{Unit}\left({R}\right)\right)\right)\to \left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)\in \left({{E}}^{\left({S}\setminus \left\{{s}\right\}\right)}\right)$
59 26 27 38 58 syl12anc
60 breq1
61 oveq1 ${⊢}{f}=\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)\to {f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)=\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)$
62 61 eqeq1d ${⊢}{f}=\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)\to \left({f}\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}↔\left({z}\in \left({S}\setminus \left\{{s}\right\}\right)⟼{inv}_{r}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({g}\left({s}\right)\right)\right){\cdot }_{{R}}{g}\left({z}\right)\right)\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{s}\right\}\right)={s}\right)$
63 60 62 anbi12d