# Metamath Proof Explorer

## Theorem linds0

Description: The empty set is always a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion linds0 ${⊢}{M}\in {V}\to \varnothing \mathrm{linIndS}{M}$

### Proof

Step Hyp Ref Expression
1 ral0 ${⊢}\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}$
2 1 2a1i ${⊢}{M}\in {V}\to \left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left(\varnothing \right)\wedge \varnothing \mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)$
3 0ex ${⊢}\varnothing \in \mathrm{V}$
4 breq1 ${⊢}{f}=\varnothing \to \left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)↔{finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left(\varnothing \right)\right)$
5 oveq1 ${⊢}{f}=\varnothing \to {f}\mathrm{linC}\left({M}\right)\varnothing =\varnothing \mathrm{linC}\left({M}\right)\varnothing$
6 5 eqeq1d ${⊢}{f}=\varnothing \to \left({f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}↔\varnothing \mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)$
7 4 6 anbi12d ${⊢}{f}=\varnothing \to \left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)↔\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left(\varnothing \right)\wedge \varnothing \mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\right)$
8 fveq1 ${⊢}{f}=\varnothing \to {f}\left({x}\right)=\varnothing \left({x}\right)$
9 8 eqeq1d ${⊢}{f}=\varnothing \to \left({f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}↔\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)$
10 9 ralbidv ${⊢}{f}=\varnothing \to \left(\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}↔\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)$
11 7 10 imbi12d ${⊢}{f}=\varnothing \to \left(\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)↔\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left(\varnothing \right)\wedge \varnothing \mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)$
12 11 ralsng ${⊢}\varnothing \in \mathrm{V}\to \left(\forall {f}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)↔\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left(\varnothing \right)\wedge \varnothing \mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)$
13 3 12 mp1i ${⊢}{M}\in {V}\to \left(\forall {f}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)↔\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left(\varnothing \right)\wedge \varnothing \mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}\varnothing \left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)$
14 2 13 mpbird ${⊢}{M}\in {V}\to \forall {f}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)$
15 fvex ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}\in \mathrm{V}$
16 map0e ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}\in \mathrm{V}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }={1}_{𝑜}$
17 15 16 mp1i ${⊢}{M}\in {V}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }={1}_{𝑜}$
18 df1o2 ${⊢}{1}_{𝑜}=\left\{\varnothing \right\}$
19 17 18 syl6eq ${⊢}{M}\in {V}\to {{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }=\left\{\varnothing \right\}$
20 19 raleqdv ${⊢}{M}\in {V}\to \left(\forall {f}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)↔\forall {f}\in \left\{\varnothing \right\}\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)$
21 14 20 mpbird ${⊢}{M}\in {V}\to \forall {f}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)$
22 0elpw ${⊢}\varnothing \in 𝒫{\mathrm{Base}}_{{M}}$
23 21 22 jctil ${⊢}{M}\in {V}\to \left(\varnothing \in 𝒫{\mathrm{Base}}_{{M}}\wedge \forall {f}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)$
24 eqid ${⊢}{\mathrm{Base}}_{{M}}={\mathrm{Base}}_{{M}}$
25 eqid ${⊢}{0}_{{M}}={0}_{{M}}$
26 eqid ${⊢}\mathrm{Scalar}\left({M}\right)=\mathrm{Scalar}\left({M}\right)$
27 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
28 eqid ${⊢}{0}_{\mathrm{Scalar}\left({M}\right)}={0}_{\mathrm{Scalar}\left({M}\right)}$
29 24 25 26 27 28 islininds ${⊢}\left(\varnothing \in \mathrm{V}\wedge {M}\in {V}\right)\to \left(\varnothing \mathrm{linIndS}{M}↔\left(\varnothing \in 𝒫{\mathrm{Base}}_{{M}}\wedge \forall {f}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)\right)$
30 3 29 mpan ${⊢}{M}\in {V}\to \left(\varnothing \mathrm{linIndS}{M}↔\left(\varnothing \in 𝒫{\mathrm{Base}}_{{M}}\wedge \forall {f}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\left(\left({finSupp}_{{0}_{\mathrm{Scalar}\left({M}\right)}}\left({f}\right)\wedge {f}\mathrm{linC}\left({M}\right)\varnothing ={0}_{{M}}\right)\to \forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={0}_{\mathrm{Scalar}\left({M}\right)}\right)\right)\right)$
31 23 30 mpbird ${⊢}{M}\in {V}\to \varnothing \mathrm{linIndS}{M}$