# Metamath Proof Explorer

## Theorem islindf4

Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses islindf4.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
islindf4.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
islindf4.t
islindf4.z
islindf4.y ${⊢}{Y}={0}_{{R}}$
islindf4.l ${⊢}{L}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{I}\right)}$
Assertion islindf4

### Proof

Step Hyp Ref Expression
1 islindf4.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 islindf4.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
3 islindf4.t
4 islindf4.z
5 islindf4.y ${⊢}{Y}={0}_{{R}}$
6 islindf4.l ${⊢}{L}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{I}\right)}$
7 raldifsni
8 simpll1 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {W}\in \mathrm{LMod}$
9 simprll ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {l}\in {\mathrm{Base}}_{{R}}$
10 ffvelrn ${⊢}\left({F}:{I}⟶{B}\wedge {j}\in {I}\right)\to {F}\left({j}\right)\in {B}$
11 10 3ad2antl3 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {F}\left({j}\right)\in {B}$
12 11 adantr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {F}\left({j}\right)\in {B}$
13 eqid ${⊢}{inv}_{g}\left({W}\right)={inv}_{g}\left({W}\right)$
14 eqid ${⊢}{inv}_{g}\left({R}\right)={inv}_{g}\left({R}\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
16 1 2 3 13 14 15 lmodvsinv
17 8 9 12 16 syl3anc
18 17 eqeq1d
19 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
20 8 19 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {W}\in \mathrm{Grp}$
21 1 2 3 15 lmodvscl
22 8 9 12 21 syl3anc
23 lmodcmn ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{CMnd}$
24 8 23 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {W}\in \mathrm{CMnd}$
25 simpll2 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {I}\in {X}$
26 difexg ${⊢}{I}\in {X}\to {I}\setminus \left\{{j}\right\}\in \mathrm{V}$
27 25 26 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {I}\setminus \left\{{j}\right\}\in \mathrm{V}$
28 simprlr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)$
29 elmapi ${⊢}{y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\to {y}:{I}\setminus \left\{{j}\right\}⟶{\mathrm{Base}}_{{R}}$
30 28 29 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {y}:{I}\setminus \left\{{j}\right\}⟶{\mathrm{Base}}_{{R}}$
31 simpll3 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {F}:{I}⟶{B}$
32 difss ${⊢}{I}\setminus \left\{{j}\right\}\subseteq {I}$
33 fssres ${⊢}\left({F}:{I}⟶{B}\wedge {I}\setminus \left\{{j}\right\}\subseteq {I}\right)\to \left({{F}↾}_{\left({I}\setminus \left\{{j}\right\}\right)}\right):{I}\setminus \left\{{j}\right\}⟶{B}$
34 31 32 33 sylancl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to \left({{F}↾}_{\left({I}\setminus \left\{{j}\right\}\right)}\right):{I}\setminus \left\{{j}\right\}⟶{B}$
35 2 15 3 1 8 30 34 27 lcomf
36 simprr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {finSupp}_{{Y}}\left({y}\right)$
37 2 15 3 1 8 30 34 27 4 5 36 lcomfsupp
38 1 4 24 27 35 37 gsumcl
39 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
40 1 39 4 13 grpinvid2
41 20 22 38 40 syl3anc
42 simplr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {j}\in {I}$
43 fsnunf2 ${⊢}\left({y}:{I}\setminus \left\{{j}\right\}⟶{\mathrm{Base}}_{{R}}\wedge {j}\in {I}\wedge {l}\in {\mathrm{Base}}_{{R}}\right)\to \left({y}\cup \left\{⟨{j},{l}⟩\right\}\right):{I}⟶{\mathrm{Base}}_{{R}}$
44 30 42 9 43 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to \left({y}\cup \left\{⟨{j},{l}⟩\right\}\right):{I}⟶{\mathrm{Base}}_{{R}}$
45 2 15 3 1 8 44 31 25 lcomf
46 simpr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {j}\in {I}$
47 simpl ${⊢}\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\to {l}\in {\mathrm{Base}}_{{R}}$
48 46 47 anim12i ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\right)\to \left({j}\in {I}\wedge {l}\in {\mathrm{Base}}_{{R}}\right)$
49 elmapfun ${⊢}{y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\to \mathrm{Fun}{y}$
50 fdm ${⊢}{y}:{I}\setminus \left\{{j}\right\}⟶{\mathrm{Base}}_{{R}}\to \mathrm{dom}{y}={I}\setminus \left\{{j}\right\}$
51 neldifsnd ${⊢}\mathrm{dom}{y}={I}\setminus \left\{{j}\right\}\to ¬{j}\in \left({I}\setminus \left\{{j}\right\}\right)$
52 df-nel ${⊢}{j}\notin \mathrm{dom}{y}↔¬{j}\in \mathrm{dom}{y}$
53 eleq2 ${⊢}\mathrm{dom}{y}={I}\setminus \left\{{j}\right\}\to \left({j}\in \mathrm{dom}{y}↔{j}\in \left({I}\setminus \left\{{j}\right\}\right)\right)$
54 53 notbid ${⊢}\mathrm{dom}{y}={I}\setminus \left\{{j}\right\}\to \left(¬{j}\in \mathrm{dom}{y}↔¬{j}\in \left({I}\setminus \left\{{j}\right\}\right)\right)$
55 52 54 syl5bb ${⊢}\mathrm{dom}{y}={I}\setminus \left\{{j}\right\}\to \left({j}\notin \mathrm{dom}{y}↔¬{j}\in \left({I}\setminus \left\{{j}\right\}\right)\right)$
56 51 55 mpbird ${⊢}\mathrm{dom}{y}={I}\setminus \left\{{j}\right\}\to {j}\notin \mathrm{dom}{y}$
57 29 50 56 3syl ${⊢}{y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\to {j}\notin \mathrm{dom}{y}$
58 49 57 jca ${⊢}{y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\to \left(\mathrm{Fun}{y}\wedge {j}\notin \mathrm{dom}{y}\right)$
59 58 adantl ${⊢}\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\to \left(\mathrm{Fun}{y}\wedge {j}\notin \mathrm{dom}{y}\right)$
60 59 adantl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\right)\to \left(\mathrm{Fun}{y}\wedge {j}\notin \mathrm{dom}{y}\right)$
61 48 60 jca ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\right)\to \left(\left({j}\in {I}\wedge {l}\in {\mathrm{Base}}_{{R}}\right)\wedge \left(\mathrm{Fun}{y}\wedge {j}\notin \mathrm{dom}{y}\right)\right)$
62 funsnfsupp ${⊢}\left(\left({j}\in {I}\wedge {l}\in {\mathrm{Base}}_{{R}}\right)\wedge \left(\mathrm{Fun}{y}\wedge {j}\notin \mathrm{dom}{y}\right)\right)\to \left({finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)↔{finSupp}_{{Y}}\left({y}\right)\right)$
63 62 bicomd ${⊢}\left(\left({j}\in {I}\wedge {l}\in {\mathrm{Base}}_{{R}}\right)\wedge \left(\mathrm{Fun}{y}\wedge {j}\notin \mathrm{dom}{y}\right)\right)\to \left({finSupp}_{{Y}}\left({y}\right)↔{finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)\right)$
64 61 63 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\right)\to \left({finSupp}_{{Y}}\left({y}\right)↔{finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)\right)$
65 64 biimpd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\right)\to \left({finSupp}_{{Y}}\left({y}\right)\to {finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)\right)$
66 65 impr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)$
67 2 15 3 1 8 44 31 25 4 5 66 lcomfsupp
68 incom ${⊢}\left({I}\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}=\left\{{j}\right\}\cap \left({I}\setminus \left\{{j}\right\}\right)$
69 disjdif ${⊢}\left\{{j}\right\}\cap \left({I}\setminus \left\{{j}\right\}\right)=\varnothing$
70 68 69 eqtri ${⊢}\left({I}\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}=\varnothing$
71 70 a1i ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to \left({I}\setminus \left\{{j}\right\}\right)\cap \left\{{j}\right\}=\varnothing$
72 difsnid ${⊢}{j}\in {I}\to \left({I}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}={I}$
73 72 eqcomd ${⊢}{j}\in {I}\to {I}=\left({I}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}$
74 42 73 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {I}=\left({I}\setminus \left\{{j}\right\}\right)\cup \left\{{j}\right\}$
75 1 4 39 24 25 45 67 71 74 gsumsplit
76 vex ${⊢}{y}\in \mathrm{V}$
77 snex ${⊢}\left\{⟨{j},{l}⟩\right\}\in \mathrm{V}$
78 76 77 unex ${⊢}{y}\cup \left\{⟨{j},{l}⟩\right\}\in \mathrm{V}$
79 simpl3 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {F}:{I}⟶{B}$
80 simpl2 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {I}\in {X}$
81 fex ${⊢}\left({F}:{I}⟶{B}\wedge {I}\in {X}\right)\to {F}\in \mathrm{V}$
82 79 80 81 syl2anc ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {F}\in \mathrm{V}$
83 82 adantr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {F}\in \mathrm{V}$
84 offres
85 78 83 84 sylancr
86 30 ffnd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {y}Fn\left({I}\setminus \left\{{j}\right\}\right)$
87 neldifsn ${⊢}¬{j}\in \left({I}\setminus \left\{{j}\right\}\right)$
88 fsnunres ${⊢}\left({y}Fn\left({I}\setminus \left\{{j}\right\}\right)\wedge ¬{j}\in \left({I}\setminus \left\{{j}\right\}\right)\right)\to {\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)↾}_{\left({I}\setminus \left\{{j}\right\}\right)}={y}$
89 86 87 88 sylancl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)↾}_{\left({I}\setminus \left\{{j}\right\}\right)}={y}$
90 89 oveq1d
91 85 90 eqtrd
92 91 oveq2d
93 45 ffnd
94 fnressn
95 93 42 94 syl2anc
96 44 ffnd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to \left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)Fn{I}$
97 31 ffnd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {F}Fn{I}$
98 fnfvof
99 96 97 25 42 98 syl22anc
100 fndm ${⊢}{y}Fn\left({I}\setminus \left\{{j}\right\}\right)\to \mathrm{dom}{y}={I}\setminus \left\{{j}\right\}$
101 100 eleq2d ${⊢}{y}Fn\left({I}\setminus \left\{{j}\right\}\right)\to \left({j}\in \mathrm{dom}{y}↔{j}\in \left({I}\setminus \left\{{j}\right\}\right)\right)$
102 87 101 mtbiri ${⊢}{y}Fn\left({I}\setminus \left\{{j}\right\}\right)\to ¬{j}\in \mathrm{dom}{y}$
103 vex ${⊢}{j}\in \mathrm{V}$
104 vex ${⊢}{l}\in \mathrm{V}$
105 fsnunfv ${⊢}\left({j}\in \mathrm{V}\wedge {l}\in \mathrm{V}\wedge ¬{j}\in \mathrm{dom}{y}\right)\to \left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)={l}$
106 103 104 105 mp3an12 ${⊢}¬{j}\in \mathrm{dom}{y}\to \left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)={l}$
107 86 102 106 3syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to \left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)={l}$
108 107 oveq1d
109 99 108 eqtrd
110 109 opeq2d
111 110 sneqd
112 ovex
113 fmptsn
114 103 112 113 mp2an
115 114 a1i
116 95 111 115 3eqtrd
117 116 oveq2d
118 cmnmnd ${⊢}{W}\in \mathrm{CMnd}\to {W}\in \mathrm{Mnd}$
119 8 23 118 3syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {W}\in \mathrm{Mnd}$
120 103 a1i ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {j}\in \mathrm{V}$
121 eqidd
122 1 121 gsumsn
123 119 120 22 122 syl3anc
124 117 123 eqtrd
125 92 124 oveq12d
126 75 125 eqtr2d
127 126 eqeq1d
128 18 41 127 3bitrd
129 107 eqcomd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to {l}=\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)$
130 129 eqeq1d ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left(\left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\wedge {finSupp}_{{Y}}\left({y}\right)\right)\right)\to \left({l}={Y}↔\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)={Y}\right)$
131 128 130 imbi12d
132 131 anassrs
133 132 pm5.74da
134 impexp
135 134 a1i
136 64 bicomd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge \left({l}\in {\mathrm{Base}}_{{R}}\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({I}\setminus \left\{{j}\right\}\right)}\right)\right)\right)\to \left({finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)↔{finSupp}_{{Y}}\left({y}\right)\right)$
137 136 imbi1d
138 133 135 137 3bitr4d
139 138 2ralbidva
140 breq1 ${⊢}{x}={y}\cup \left\{⟨{j},{l}⟩\right\}\to \left({finSupp}_{{Y}}\left({x}\right)↔{finSupp}_{{Y}}\left(\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\right)\right)$
141 oveq1
142 141 oveq2d
143 142 eqeq1d
144 fveq1 ${⊢}{x}={y}\cup \left\{⟨{j},{l}⟩\right\}\to {x}\left({j}\right)=\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)$
145 144 eqeq1d ${⊢}{x}={y}\cup \left\{⟨{j},{l}⟩\right\}\to \left({x}\left({j}\right)={Y}↔\left({y}\cup \left\{⟨{j},{l}⟩\right\}\right)\left({j}\right)={Y}\right)$
146 143 145 imbi12d
147 140 146 imbi12d
148 147 ralxpmap
150 139 149 bitr4d
151 breq1 ${⊢}{z}={x}\to \left({finSupp}_{{Y}}\left({z}\right)↔{finSupp}_{{Y}}\left({x}\right)\right)$
152 151 ralrab
153 150 152 syl6bbr
154 resima ${⊢}\left({{F}↾}_{\left({I}\setminus \left\{{j}\right\}\right)}\right)\left[{I}\setminus \left\{{j}\right\}\right]={F}\left[{I}\setminus \left\{{j}\right\}\right]$
155 154 eqcomi ${⊢}{F}\left[{I}\setminus \left\{{j}\right\}\right]=\left({{F}↾}_{\left({I}\setminus \left\{{j}\right\}\right)}\right)\left[{I}\setminus \left\{{j}\right\}\right]$
156 155 fveq2i ${⊢}\mathrm{LSpan}\left({W}\right)\left({F}\left[{I}\setminus \left\{{j}\right\}\right]\right)=\mathrm{LSpan}\left({W}\right)\left(\left({{F}↾}_{\left({I}\setminus \left\{{j}\right\}\right)}\right)\left[{I}\setminus \left\{{j}\right\}\right]\right)$
157 156 eleq2i
158 eqid ${⊢}\mathrm{LSpan}\left({W}\right)=\mathrm{LSpan}\left({W}\right)$
159 79 32 33 sylancl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to \left({{F}↾}_{\left({I}\setminus \left\{{j}\right\}\right)}\right):{I}\setminus \left\{{j}\right\}⟶{B}$
160 simpl1 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {W}\in \mathrm{LMod}$
161 26 3ad2ant2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\to {I}\setminus \left\{{j}\right\}\in \mathrm{V}$
162 161 adantr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {I}\setminus \left\{{j}\right\}\in \mathrm{V}$
163 158 1 15 2 5 3 159 160 162 ellspd
164 157 163 syl5bb
165 164 imbi1d
166 r19.23v
167 165 166 syl6bbr
168 167 ralbidv
169 2 fvexi ${⊢}{R}\in \mathrm{V}$
170 eqid ${⊢}{R}\mathrm{freeLMod}{I}={R}\mathrm{freeLMod}{I}$
171 eqid ${⊢}\left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}=\left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}$
172 170 15 5 171 frlmbas ${⊢}\left({R}\in \mathrm{V}\wedge {I}\in {X}\right)\to \left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{I}\right)}$
173 169 172 mpan ${⊢}{I}\in {X}\to \left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{I}\right)}$
174 173 3ad2ant2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\to \left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{I}\right)}$
175 174 adantr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to \left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{I}\right)}$
176 175 6 syl6reqr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\to {L}=\left\{{z}\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)|{finSupp}_{{Y}}\left({z}\right)\right\}$
177 176 raleqdv
178 153 168 177 3bitr4d
179 7 178 syl5bb
180 2 lmodfgrp ${⊢}{W}\in \mathrm{LMod}\to {R}\in \mathrm{Grp}$
181 15 5 14 grpinvnzcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {l}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to {inv}_{g}\left({R}\right)\left({l}\right)\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)$
182 180 181 sylan ${⊢}\left({W}\in \mathrm{LMod}\wedge {l}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to {inv}_{g}\left({R}\right)\left({l}\right)\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)$
183 15 5 14 grpinvnzcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {k}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to {inv}_{g}\left({R}\right)\left({k}\right)\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)$
184 180 183 sylan ${⊢}\left({W}\in \mathrm{LMod}\wedge {k}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to {inv}_{g}\left({R}\right)\left({k}\right)\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)$
185 eldifi ${⊢}{k}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\to {k}\in {\mathrm{Base}}_{{R}}$
186 15 14 grpinvinv ${⊢}\left({R}\in \mathrm{Grp}\wedge {k}\in {\mathrm{Base}}_{{R}}\right)\to {inv}_{g}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({k}\right)\right)={k}$
187 180 185 186 syl2an ${⊢}\left({W}\in \mathrm{LMod}\wedge {k}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to {inv}_{g}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({k}\right)\right)={k}$
188 187 eqcomd ${⊢}\left({W}\in \mathrm{LMod}\wedge {k}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to {k}={inv}_{g}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({k}\right)\right)$
189 fveq2 ${⊢}{l}={inv}_{g}\left({R}\right)\left({k}\right)\to {inv}_{g}\left({R}\right)\left({l}\right)={inv}_{g}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({k}\right)\right)$
190 189 rspceeqv ${⊢}\left({inv}_{g}\left({R}\right)\left({k}\right)\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\wedge {k}={inv}_{g}\left({R}\right)\left({inv}_{g}\left({R}\right)\left({k}\right)\right)\right)\to \exists {l}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\phantom{\rule{.4em}{0ex}}{k}={inv}_{g}\left({R}\right)\left({l}\right)$
191 184 188 190 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {k}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\right)\to \exists {l}\in \left({\mathrm{Base}}_{{R}}\setminus \left\{{Y}\right\}\right)\phantom{\rule{.4em}{0ex}}{k}={inv}_{g}\left({R}\right)\left({l}\right)$
192 oveq1
193 192 eleq1d
194 193 notbid
196 182 191 195 ralxfrd
199 simplr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge {x}\in {L}\right)\to {j}\in {I}$
200 5 fvexi ${⊢}{Y}\in \mathrm{V}$
201 200 fvconst2 ${⊢}{j}\in {I}\to \left({I}×\left\{{Y}\right\}\right)\left({j}\right)={Y}$
202 199 201 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge {x}\in {L}\right)\to \left({I}×\left\{{Y}\right\}\right)\left({j}\right)={Y}$
203 202 eqeq2d ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {j}\in {I}\right)\wedge {x}\in {L}\right)\to \left({x}\left({j}\right)=\left({I}×\left\{{Y}\right\}\right)\left({j}\right)↔{x}\left({j}\right)={Y}\right)$
204 203 imbi2d
205 204 ralbidva
206 179 198 205 3bitr4d
207 206 ralbidva
208 1 3 158 2 15 5 islindf2
209 170 15 6 frlmbasf ${⊢}\left({I}\in {X}\wedge {x}\in {L}\right)\to {x}:{I}⟶{\mathrm{Base}}_{{R}}$
210 209 3ad2antl2 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {x}\in {L}\right)\to {x}:{I}⟶{\mathrm{Base}}_{{R}}$
211 210 ffnd ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {x}\in {L}\right)\to {x}Fn{I}$
212 fnconstg ${⊢}{Y}\in \mathrm{V}\to \left({I}×\left\{{Y}\right\}\right)Fn{I}$
213 200 212 ax-mp ${⊢}\left({I}×\left\{{Y}\right\}\right)Fn{I}$
214 eqfnfv ${⊢}\left({x}Fn{I}\wedge \left({I}×\left\{{Y}\right\}\right)Fn{I}\right)\to \left({x}={I}×\left\{{Y}\right\}↔\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)=\left({I}×\left\{{Y}\right\}\right)\left({j}\right)\right)$
215 211 213 214 sylancl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {I}\in {X}\wedge {F}:{I}⟶{B}\right)\wedge {x}\in {L}\right)\to \left({x}={I}×\left\{{Y}\right\}↔\forall {j}\in {I}\phantom{\rule{.4em}{0ex}}{x}\left({j}\right)=\left({I}×\left\{{Y}\right\}\right)\left({j}\right)\right)$
216 215 imbi2d
217 216 ralbidva
218 r19.21v
219 218 ralbii
220 ralcom
221 219 220 bitr3i
222 217 221 syl6bb
223 207 208 222 3bitr4d