# Metamath Proof Explorer

## Theorem lincresunit2

Description: Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-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 lincresunit2

### 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 difexg ${⊢}{S}\in 𝒫{B}\to {S}\setminus \left\{{X}\right\}\in \mathrm{V}$
12 11 3ad2ant1 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {S}\setminus \left\{{X}\right\}\in \mathrm{V}$
13 12 adantl ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {S}\setminus \left\{{X}\right\}\in \mathrm{V}$
15 mptexg
16 10 15 eqeltrid ${⊢}{S}\setminus \left\{{X}\right\}\in \mathrm{V}\to {G}\in \mathrm{V}$
17 14 16 syl
18 10 funmpt2 ${⊢}\mathrm{Fun}{G}$
19 18 a1i
20 5 fvexi
21 20 a1i
22 simpr
23 22 fsuppimpd
24 simplr ${⊢}\left(\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\wedge {s}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)$
25 simpll ${⊢}\left(\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\wedge {s}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to \left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)$
26 eldifi ${⊢}{s}\in \left({S}\setminus \left\{{X}\right\}\right)\to {s}\in {S}$
27 26 adantl ${⊢}\left(\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\wedge {s}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to {s}\in {S}$
28 1 2 3 4 5 6 7 8 9 10 lincresunitlem2
29 24 25 27 28 syl21anc
30 29 ralrimiva
31 10 fnmpt
32 30 31 syl ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {G}Fn\left({S}\setminus \left\{{X}\right\}\right)$
33 elmapfn ${⊢}{F}\in \left({{E}}^{{S}}\right)\to {F}Fn{S}$
34 33 adantr ${⊢}\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\to {F}Fn{S}$
35 34 adantr ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {F}Fn{S}$
36 32 35 jca ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to \left({G}Fn\left({S}\setminus \left\{{X}\right\}\right)\wedge {F}Fn{S}\right)$
37 difssd ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {S}\setminus \left\{{X}\right\}\subseteq {S}$
38 simpr1 ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {S}\in 𝒫{B}$
39 20 a1i
40 37 38 39 3jca
41 fveq2 ${⊢}{s}={x}\to {F}\left({s}\right)={F}\left({x}\right)$
42 41 oveq2d
43 simplr
44 simpllr
45 simpll ${⊢}\left(\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\wedge {x}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to \left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)$
47 eldifi ${⊢}{x}\in \left({S}\setminus \left\{{X}\right\}\right)\to {x}\in {S}$
48 47 adantl ${⊢}\left(\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\wedge {x}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to {x}\in {S}$
50 1 2 3 4 5 6 7 8 9 10 lincresunitlem2
51 44 46 49 50 syl21anc
52 10 42 43 51 fvmptd3
53 oveq2
54 2 lmodring ${⊢}{M}\in \mathrm{LMod}\to {R}\in \mathrm{Ring}$
55 54 3ad2ant2 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {R}\in \mathrm{Ring}$
56 55 adantl ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {R}\in \mathrm{Ring}$
57 1 2 3 4 5 6 7 8 9 10 lincresunitlem1 ${⊢}\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 {I}\left({N}\left({F}\left({X}\right)\right)\right)\in {E}$
58 57 ancoms ${⊢}\left(\left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)\wedge \left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\right)\to {I}\left({N}\left({F}\left({X}\right)\right)\right)\in {E}$
59 3 9 5 ringrz
60 56 58 59 syl2anc
62 53 61 sylan9eqr
63 52 62 eqtrd
64 63 ex
65 64 ralrimiva
66 suppfnss
67 66 imp
68 36 40 65 67 syl21anc