Metamath Proof Explorer

Theorem islinindfis

Description: The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 islininds.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 islininds.z ${⊢}{Z}={0}_{{M}}$
3 islininds.r ${⊢}{R}=\mathrm{Scalar}\left({M}\right)$
4 islininds.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
5 islininds.0
6 1 2 3 4 5 islininds
7 pm4.79
8 elmapi ${⊢}{f}\in \left({{E}}^{{S}}\right)\to {f}:{S}⟶{E}$
9 8 adantl ${⊢}\left(\left({S}\in \mathrm{Fin}\wedge {M}\in {W}\right)\wedge {f}\in \left({{E}}^{{S}}\right)\right)\to {f}:{S}⟶{E}$
10 simpll ${⊢}\left(\left({S}\in \mathrm{Fin}\wedge {M}\in {W}\right)\wedge {f}\in \left({{E}}^{{S}}\right)\right)\to {S}\in \mathrm{Fin}$
11 5 fvexi
12 11 a1i
13 9 10 12 fdmfifsupp