# Metamath Proof Explorer

## Theorem lincresunit3lem2

Description: Lemma 2 for lincresunit3 . (Contributed by AV, 18-May-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses lincresunit.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
lincresunit.r ${⊢}{R}=\mathrm{Scalar}\left({M}\right)$
lincresunit.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
lincresunit.u ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
lincresunit.0
lincresunit.z ${⊢}{Z}={0}_{{M}}$
lincresunit.n ${⊢}{N}={inv}_{g}\left({R}\right)$
lincresunit.i ${⊢}{I}={inv}_{r}\left({R}\right)$
lincresunit.t
lincresunit.g
Assertion lincresunit3lem2

### Proof

Step Hyp Ref Expression
1 lincresunit.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 lincresunit.r ${⊢}{R}=\mathrm{Scalar}\left({M}\right)$
3 lincresunit.e ${⊢}{E}={\mathrm{Base}}_{{R}}$
4 lincresunit.u ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
5 lincresunit.0
6 lincresunit.z ${⊢}{Z}={0}_{{M}}$
7 lincresunit.n ${⊢}{N}={inv}_{g}\left({R}\right)$
8 lincresunit.i ${⊢}{I}={inv}_{r}\left({R}\right)$
9 lincresunit.t
10 lincresunit.g
11 simpl2
12 2 fveq2i ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
13 3 12 eqtri ${⊢}{E}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
14 13 oveq1i ${⊢}{{E}}^{{S}}={{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{{S}}$
15 14 eleq2i ${⊢}{F}\in \left({{E}}^{{S}}\right)↔{F}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{{S}}\right)$
16 15 biimpi ${⊢}{F}\in \left({{E}}^{{S}}\right)\to {F}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{{S}}\right)$
19 difssd
20 elmapssres ${⊢}\left({F}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{{S}}\right)\wedge {S}\setminus \left\{{X}\right\}\subseteq {S}\right)\to {{F}↾}_{\left({S}\setminus \left\{{X}\right\}\right)}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\left({S}\setminus \left\{{X}\right\}\right)}\right)$
21 18 19 20 syl2anc
22 elpwi ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}\to {S}\subseteq {\mathrm{Base}}_{{M}}$
23 22 ssdifssd ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}\to {S}\setminus \left\{{X}\right\}\subseteq {\mathrm{Base}}_{{M}}$
24 difexg ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}\to {S}\setminus \left\{{X}\right\}\in \mathrm{V}$
25 elpwg ${⊢}{S}\setminus \left\{{X}\right\}\in \mathrm{V}\to \left({S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}↔{S}\setminus \left\{{X}\right\}\subseteq {\mathrm{Base}}_{{M}}\right)$
26 24 25 syl ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}\to \left({S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}↔{S}\setminus \left\{{X}\right\}\subseteq {\mathrm{Base}}_{{M}}\right)$
27 23 26 mpbird ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}\to {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}$
28 1 pweqi ${⊢}𝒫{B}=𝒫{\mathrm{Base}}_{{M}}$
29 27 28 eleq2s ${⊢}{S}\in 𝒫{B}\to {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}$
30 29 3ad2ant1 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}$
32 lincval ${⊢}\left({M}\in \mathrm{LMod}\wedge {{F}↾}_{\left({S}\setminus \left\{{X}\right\}\right)}\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}}^{\left({S}\setminus \left\{{X}\right\}\right)}\right)\wedge {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}\right)\to \left({{F}↾}_{\left({S}\setminus \left\{{X}\right\}\right)}\right)\mathrm{linC}\left({M}\right)\left({S}\setminus \left\{{X}\right\}\right)=\underset{{z}\in {S}\setminus \left\{{X}\right\}}{{\sum }_{{M}}}\left(\left({{F}↾}_{\left({S}\setminus \left\{{X}\right\}\right)}\right)\left({z}\right){\cdot }_{{M}}{z}\right)$
33 11 21 31 32 syl3anc
34 simpll
35 simplr1
36 simplr2
37 simpr
38 1 2 3 4 5 6 7 8 9 10 lincresunit3lem1 ${⊢}\left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\wedge \left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\wedge {z}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\right)\to {N}\left({F}\left({X}\right)\right){\cdot }_{{M}}\left({G}\left({z}\right){\cdot }_{{M}}{z}\right)={F}\left({z}\right){\cdot }_{{M}}{z}$
39 34 35 36 37 38 syl13anc
40 fvres ${⊢}{z}\in \left({S}\setminus \left\{{X}\right\}\right)\to \left({{F}↾}_{\left({S}\setminus \left\{{X}\right\}\right)}\right)\left({z}\right)={F}\left({z}\right)$
42 41 eqcomd
43 42 oveq1d
44 39 43 eqtrd
45 44 mpteq2dva
46 45 oveq2d
47 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
48 eqid ${⊢}{\cdot }_{{M}}={\cdot }_{{M}}$
49 difexg ${⊢}{S}\in 𝒫{B}\to {S}\setminus \left\{{X}\right\}\in \mathrm{V}$
50 49 3ad2ant1 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {S}\setminus \left\{{X}\right\}\in \mathrm{V}$
52 2 lmodfgrp ${⊢}{M}\in \mathrm{LMod}\to {R}\in \mathrm{Grp}$
53 52 3ad2ant2 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {R}\in \mathrm{Grp}$
54 53 adantr ${⊢}\left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\wedge {F}\in \left({{E}}^{{S}}\right)\right)\to {R}\in \mathrm{Grp}$
55 elmapi ${⊢}{F}\in \left({{E}}^{{S}}\right)\to {F}:{S}⟶{E}$
56 ffvelrn ${⊢}\left({F}:{S}⟶{E}\wedge {X}\in {S}\right)\to {F}\left({X}\right)\in {E}$
57 56 expcom ${⊢}{X}\in {S}\to \left({F}:{S}⟶{E}\to {F}\left({X}\right)\in {E}\right)$
58 57 3ad2ant3 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to \left({F}:{S}⟶{E}\to {F}\left({X}\right)\in {E}\right)$
59 55 58 syl5com ${⊢}{F}\in \left({{E}}^{{S}}\right)\to \left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {F}\left({X}\right)\in {E}\right)$
60 59 impcom ${⊢}\left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\wedge {F}\in \left({{E}}^{{S}}\right)\right)\to {F}\left({X}\right)\in {E}$
61 3 7 grpinvcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {F}\left({X}\right)\in {E}\right)\to {N}\left({F}\left({X}\right)\right)\in {E}$
62 54 60 61 syl2anc ${⊢}\left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\wedge {F}\in \left({{E}}^{{S}}\right)\right)\to {N}\left({F}\left({X}\right)\right)\in {E}$
65 1 2 3 4 5 6 7 8 9 10 lincresunit1 ${⊢}\left(\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\wedge \left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\right)\to {G}\in \left({{E}}^{\left({S}\setminus \left\{{X}\right\}\right)}\right)$
67 elmapi ${⊢}{G}\in \left({{E}}^{\left({S}\setminus \left\{{X}\right\}\right)}\right)\to {G}:{S}\setminus \left\{{X}\right\}⟶{E}$
68 ffvelrn ${⊢}\left({G}:{S}\setminus \left\{{X}\right\}⟶{E}\wedge {z}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to {G}\left({z}\right)\in {E}$
69 68 ex ${⊢}{G}:{S}\setminus \left\{{X}\right\}⟶{E}\to \left({z}\in \left({S}\setminus \left\{{X}\right\}\right)\to {G}\left({z}\right)\in {E}\right)$
70 66 67 69 3syl
71 70 imp
72 elpwi ${⊢}{S}\in 𝒫{B}\to {S}\subseteq {B}$
73 eldifi ${⊢}{z}\in \left({S}\setminus \left\{{X}\right\}\right)\to {z}\in {S}$
74 ssel2 ${⊢}\left({S}\subseteq {B}\wedge {z}\in {S}\right)\to {z}\in {B}$
75 74 expcom ${⊢}{z}\in {S}\to \left({S}\subseteq {B}\to {z}\in {B}\right)$
76 73 75 syl ${⊢}{z}\in \left({S}\setminus \left\{{X}\right\}\right)\to \left({S}\subseteq {B}\to {z}\in {B}\right)$
77 72 76 syl5com ${⊢}{S}\in 𝒫{B}\to \left({z}\in \left({S}\setminus \left\{{X}\right\}\right)\to {z}\in {B}\right)$
78 77 3ad2ant1 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to \left({z}\in \left({S}\setminus \left\{{X}\right\}\right)\to {z}\in {B}\right)$
81 1 2 48 3 lmodvscl ${⊢}\left({M}\in \mathrm{LMod}\wedge {G}\left({z}\right)\in {E}\wedge {z}\in {B}\right)\to {G}\left({z}\right){\cdot }_{{M}}{z}\in {B}$
83 simp2 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {M}\in \mathrm{LMod}$
84 83 30 jca ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to \left({M}\in \mathrm{LMod}\wedge {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}\right)$
88 2 3 scmfsupp ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}\right)\wedge {G}\in \left({{E}}^{\left({S}\setminus \left\{{X}\right\}\right)}\right)\wedge {finSupp}_{{0}_{{R}}}\left({G}\right)\right)\to {finSupp}_{{0}_{{M}}}\left(\left({z}\in \left({S}\setminus \left\{{X}\right\}\right)⟼{G}\left({z}\right){\cdot }_{{M}}{z}\right)\right)$
89 88 6 breqtrrdi ${⊢}\left(\left({M}\in \mathrm{LMod}\wedge {S}\setminus \left\{{X}\right\}\in 𝒫{\mathrm{Base}}_{{M}}\right)\wedge {G}\in \left({{E}}^{\left({S}\setminus \left\{{X}\right\}\right)}\right)\wedge {finSupp}_{{0}_{{R}}}\left({G}\right)\right)\to {finSupp}_{{Z}}\left(\left({z}\in \left({S}\setminus \left\{{X}\right\}\right)⟼{G}\left({z}\right){\cdot }_{{M}}{z}\right)\right)$