# Metamath Proof Explorer

## Theorem frlmlbs

Description: The unit vectors comprise a basis for a free module. (Contributed by Stefan O'Rear, 6-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmlbs.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
frlmlbs.u ${⊢}{U}={R}\mathrm{unitVec}{I}$
frlmlbs.j ${⊢}{J}=\mathrm{LBasis}\left({F}\right)$
Assertion frlmlbs ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \mathrm{ran}{U}\in {J}$

### Proof

Step Hyp Ref Expression
1 frlmlbs.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 frlmlbs.u ${⊢}{U}={R}\mathrm{unitVec}{I}$
3 frlmlbs.j ${⊢}{J}=\mathrm{LBasis}\left({F}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
5 2 1 4 uvcff ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {U}:{I}⟶{\mathrm{Base}}_{{F}}$
6 5 frnd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \mathrm{ran}{U}\subseteq {\mathrm{Base}}_{{F}}$
7 suppssdm ${⊢}{a}\mathrm{supp}{0}_{{R}}\subseteq \mathrm{dom}{a}$
8 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
9 1 8 4 frlmbasf ${⊢}\left({I}\in {V}\wedge {a}\in {\mathrm{Base}}_{{F}}\right)\to {a}:{I}⟶{\mathrm{Base}}_{{R}}$
10 9 adantll ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge {a}\in {\mathrm{Base}}_{{F}}\right)\to {a}:{I}⟶{\mathrm{Base}}_{{R}}$
11 7 10 fssdm ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge {a}\in {\mathrm{Base}}_{{F}}\right)\to {a}\mathrm{supp}{0}_{{R}}\subseteq {I}$
12 11 ralrimiva ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \forall {a}\in {\mathrm{Base}}_{{F}}\phantom{\rule{.4em}{0ex}}{a}\mathrm{supp}{0}_{{R}}\subseteq {I}$
13 rabid2 ${⊢}{\mathrm{Base}}_{{F}}=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\right\}↔\forall {a}\in {\mathrm{Base}}_{{F}}\phantom{\rule{.4em}{0ex}}{a}\mathrm{supp}{0}_{{R}}\subseteq {I}$
14 12 13 sylibr ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {\mathrm{Base}}_{{F}}=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\right\}$
15 ssid ${⊢}{I}\subseteq {I}$
16 eqid ${⊢}\mathrm{LSpan}\left({F}\right)=\mathrm{LSpan}\left({F}\right)$
17 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
18 eqid ${⊢}\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\right\}=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\right\}$
19 1 2 16 4 17 18 frlmsslsp ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {I}\subseteq {I}\right)\to \mathrm{LSpan}\left({F}\right)\left({U}\left[{I}\right]\right)=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\right\}$
20 15 19 mp3an3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \mathrm{LSpan}\left({F}\right)\left({U}\left[{I}\right]\right)=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\right\}$
21 ffn ${⊢}{U}:{I}⟶{\mathrm{Base}}_{{F}}\to {U}Fn{I}$
22 fnima ${⊢}{U}Fn{I}\to {U}\left[{I}\right]=\mathrm{ran}{U}$
23 5 21 22 3syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {U}\left[{I}\right]=\mathrm{ran}{U}$
24 23 fveq2d ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \mathrm{LSpan}\left({F}\right)\left({U}\left[{I}\right]\right)=\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\right)$
25 14 20 24 3eqtr2rd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\right)={\mathrm{Base}}_{{F}}$
26 eqid ${⊢}{\cdot }_{{F}}={\cdot }_{{F}}$
27 eqid ${⊢}\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\setminus \left\{{c}\right\}\right\}=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\setminus \left\{{c}\right\}\right\}$
28 simpll ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {R}\in \mathrm{Ring}$
29 simplr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {I}\in {V}$
30 difssd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {I}\setminus \left\{{c}\right\}\subseteq {I}$
31 vsnid ${⊢}{c}\in \left\{{c}\right\}$
32 snssi ${⊢}{c}\in {I}\to \left\{{c}\right\}\subseteq {I}$
33 32 ad2antrl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to \left\{{c}\right\}\subseteq {I}$
34 dfss4 ${⊢}\left\{{c}\right\}\subseteq {I}↔{I}\setminus \left({I}\setminus \left\{{c}\right\}\right)=\left\{{c}\right\}$
35 33 34 sylib ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {I}\setminus \left({I}\setminus \left\{{c}\right\}\right)=\left\{{c}\right\}$
36 31 35 eleqtrrid ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {c}\in \left({I}\setminus \left({I}\setminus \left\{{c}\right\}\right)\right)$
37 1 frlmsca ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {R}=\mathrm{Scalar}\left({F}\right)$
38 37 fveq2d ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
39 37 fveq2d ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {0}_{{R}}={0}_{\mathrm{Scalar}\left({F}\right)}$
40 39 sneqd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \left\{{0}_{{R}}\right\}=\left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}$
41 38 40 difeq12d ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}$
42 41 eleq2d ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \left({b}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)↔{b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)$
43 42 biimpar ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\to {b}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)$
44 43 adantrl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {b}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)$
45 1 2 4 8 26 17 27 28 29 30 36 44 frlmssuvc2 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to ¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\setminus \left\{{c}\right\}\right\}$
46 17 8 ringelnzr ${⊢}\left({R}\in \mathrm{Ring}\wedge {b}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)\to {R}\in \mathrm{NzRing}$
47 28 44 46 syl2anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {R}\in \mathrm{NzRing}$
48 2 1 4 uvcf1 ${⊢}\left({R}\in \mathrm{NzRing}\wedge {I}\in {V}\right)\to {U}:{I}\underset{1-1}{⟶}{\mathrm{Base}}_{{F}}$
49 47 29 48 syl2anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {U}:{I}\underset{1-1}{⟶}{\mathrm{Base}}_{{F}}$
50 df-f1 ${⊢}{U}:{I}\underset{1-1}{⟶}{\mathrm{Base}}_{{F}}↔\left({U}:{I}⟶{\mathrm{Base}}_{{F}}\wedge \mathrm{Fun}{{U}}^{-1}\right)$
51 50 simprbi ${⊢}{U}:{I}\underset{1-1}{⟶}{\mathrm{Base}}_{{F}}\to \mathrm{Fun}{{U}}^{-1}$
52 imadif ${⊢}\mathrm{Fun}{{U}}^{-1}\to {U}\left[{I}\setminus \left\{{c}\right\}\right]={U}\left[{I}\right]\setminus {U}\left[\left\{{c}\right\}\right]$
53 49 51 52 3syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {U}\left[{I}\setminus \left\{{c}\right\}\right]={U}\left[{I}\right]\setminus {U}\left[\left\{{c}\right\}\right]$
54 f1fn ${⊢}{U}:{I}\underset{1-1}{⟶}{\mathrm{Base}}_{{F}}\to {U}Fn{I}$
55 49 54 22 3syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {U}\left[{I}\right]=\mathrm{ran}{U}$
56 49 54 syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {U}Fn{I}$
57 simprl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {c}\in {I}$
58 fnsnfv ${⊢}\left({U}Fn{I}\wedge {c}\in {I}\right)\to \left\{{U}\left({c}\right)\right\}={U}\left[\left\{{c}\right\}\right]$
59 56 57 58 syl2anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to \left\{{U}\left({c}\right)\right\}={U}\left[\left\{{c}\right\}\right]$
60 59 eqcomd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {U}\left[\left\{{c}\right\}\right]=\left\{{U}\left({c}\right)\right\}$
61 55 60 difeq12d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to {U}\left[{I}\right]\setminus {U}\left[\left\{{c}\right\}\right]=\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}$
62 53 61 eqtr2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to \mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}={U}\left[{I}\setminus \left\{{c}\right\}\right]$
63 62 fveq2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)=\mathrm{LSpan}\left({F}\right)\left({U}\left[{I}\setminus \left\{{c}\right\}\right]\right)$
64 1 2 16 4 17 27 frlmsslsp ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {I}\setminus \left\{{c}\right\}\subseteq {I}\right)\to \mathrm{LSpan}\left({F}\right)\left({U}\left[{I}\setminus \left\{{c}\right\}\right]\right)=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\setminus \left\{{c}\right\}\right\}$
65 28 29 30 64 syl3anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to \mathrm{LSpan}\left({F}\right)\left({U}\left[{I}\setminus \left\{{c}\right\}\right]\right)=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\setminus \left\{{c}\right\}\right\}$
66 63 65 eqtrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)=\left\{{a}\in {\mathrm{Base}}_{{F}}|{a}\mathrm{supp}{0}_{{R}}\subseteq {I}\setminus \left\{{c}\right\}\right\}$
67 45 66 neleqtrrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\wedge \left({c}\in {I}\wedge {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\right)\right)\to ¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)$
68 67 ralrimivva ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \forall {c}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)$
69 oveq2 ${⊢}{a}={U}\left({c}\right)\to {b}{\cdot }_{{F}}{a}={b}{\cdot }_{{F}}{U}\left({c}\right)$
70 sneq ${⊢}{a}={U}\left({c}\right)\to \left\{{a}\right\}=\left\{{U}\left({c}\right)\right\}$
71 70 difeq2d ${⊢}{a}={U}\left({c}\right)\to \mathrm{ran}{U}\setminus \left\{{a}\right\}=\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}$
72 71 fveq2d ${⊢}{a}={U}\left({c}\right)\to \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)=\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)$
73 69 72 eleq12d ${⊢}{a}={U}\left({c}\right)\to \left({b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)↔{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)\right)$
74 73 notbid ${⊢}{a}={U}\left({c}\right)\to \left(¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)↔¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)\right)$
75 74 ralbidv ${⊢}{a}={U}\left({c}\right)\to \left(\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)↔\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)\right)$
76 75 ralrn ${⊢}{U}Fn{I}\to \left(\forall {a}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)↔\forall {c}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)\right)$
77 5 21 76 3syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \left(\forall {a}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)↔\forall {c}\in {I}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{U}\left({c}\right)\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{U}\left({c}\right)\right\}\right)\right)$
78 68 77 mpbird ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \forall {a}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)$
79 1 ovexi ${⊢}{F}\in \mathrm{V}$
80 eqid ${⊢}\mathrm{Scalar}\left({F}\right)=\mathrm{Scalar}\left({F}\right)$
81 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
82 eqid ${⊢}{0}_{\mathrm{Scalar}\left({F}\right)}={0}_{\mathrm{Scalar}\left({F}\right)}$
83 4 80 26 81 3 16 82 islbs ${⊢}{F}\in \mathrm{V}\to \left(\mathrm{ran}{U}\in {J}↔\left(\mathrm{ran}{U}\subseteq {\mathrm{Base}}_{{F}}\wedge \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\right)={\mathrm{Base}}_{{F}}\wedge \forall {a}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)\right)\right)$
84 79 83 ax-mp ${⊢}\mathrm{ran}{U}\in {J}↔\left(\mathrm{ran}{U}\subseteq {\mathrm{Base}}_{{F}}\wedge \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\right)={\mathrm{Base}}_{{F}}\wedge \forall {a}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}\setminus \left\{{0}_{\mathrm{Scalar}\left({F}\right)}\right\}\right)\phantom{\rule{.4em}{0ex}}¬{b}{\cdot }_{{F}}{a}\in \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}{U}\setminus \left\{{a}\right\}\right)\right)$
85 6 25 78 84 syl3anbrc ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to \mathrm{ran}{U}\in {J}$