# Metamath Proof Explorer

## Theorem lincresunit3lem1

Description: Lemma 1 for lincresunit3 . (Contributed by AV, 17-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 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}$

### 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 fveq2 ${⊢}{s}={z}\to {F}\left({s}\right)={F}\left({z}\right)$
12 11 oveq2d
13 simpr3 ${⊢}\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 {z}\in \left({S}\setminus \left\{{X}\right\}\right)$
14 ovexd
15 10 12 13 14 fvmptd3
16 15 oveq1d
17 16 oveq2d
18 simp2 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {M}\in \mathrm{LMod}$
19 18 adantr ${⊢}\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 {M}\in \mathrm{LMod}$
20 2 lmodfgrp ${⊢}{M}\in \mathrm{LMod}\to {R}\in \mathrm{Grp}$
21 20 3ad2ant2 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {R}\in \mathrm{Grp}$
22 3 4 unitcl ${⊢}{F}\left({X}\right)\in {U}\to {F}\left({X}\right)\in {E}$
23 22 3ad2ant2 ${⊢}\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)\to {F}\left({X}\right)\in {E}$
24 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}$
25 21 23 24 syl2an ${⊢}\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)\in {E}$
26 3simpa ${⊢}\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)\to \left({F}\in \left({{E}}^{{S}}\right)\wedge {F}\left({X}\right)\in {U}\right)$
27 26 anim2i ${⊢}\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 \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)$
28 eldifi ${⊢}{z}\in \left({S}\setminus \left\{{X}\right\}\right)\to {z}\in {S}$
29 28 3ad2ant3 ${⊢}\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)\to {z}\in {S}$
30 29 adantl ${⊢}\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 {z}\in {S}$
31 1 2 3 4 5 6 7 8 9 10 lincresunitlem2
32 27 30 31 syl2anc
33 elpwi ${⊢}{S}\in 𝒫{B}\to {S}\subseteq {B}$
34 33 sseld ${⊢}{S}\in 𝒫{B}\to \left({z}\in {S}\to {z}\in {B}\right)$
35 28 34 syl5com ${⊢}{z}\in \left({S}\setminus \left\{{X}\right\}\right)\to \left({S}\in 𝒫{B}\to {z}\in {B}\right)$
36 35 3ad2ant3 ${⊢}\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)\to \left({S}\in 𝒫{B}\to {z}\in {B}\right)$
37 36 com12 ${⊢}{S}\in 𝒫{B}\to \left(\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)\to {z}\in {B}\right)$
38 37 3ad2ant1 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to \left(\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)\to {z}\in {B}\right)$
39 38 imp ${⊢}\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 {z}\in {B}$
40 eqid ${⊢}{\cdot }_{{M}}={\cdot }_{{M}}$
41 1 2 40 3 9 lmodvsass
42 41 eqcomd
43 19 25 32 39 42 syl13anc
44 2 lmodring ${⊢}{M}\in \mathrm{LMod}\to {R}\in \mathrm{Ring}$
45 44 3ad2ant2 ${⊢}\left({S}\in 𝒫{B}\wedge {M}\in \mathrm{LMod}\wedge {X}\in {S}\right)\to {R}\in \mathrm{Ring}$
46 45 adantr ${⊢}\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 {R}\in \mathrm{Ring}$
47 elmapi ${⊢}{F}\in \left({{E}}^{{S}}\right)\to {F}:{S}⟶{E}$
48 ffvelrn ${⊢}\left({F}:{S}⟶{E}\wedge {z}\in {S}\right)\to {F}\left({z}\right)\in {E}$
49 47 28 48 syl2an ${⊢}\left({F}\in \left({{E}}^{{S}}\right)\wedge {z}\in \left({S}\setminus \left\{{X}\right\}\right)\right)\to {F}\left({z}\right)\in {E}$
50 49 3adant2 ${⊢}\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)\to {F}\left({z}\right)\in {E}$
51 50 adantl ${⊢}\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 {F}\left({z}\right)\in {E}$
52 simp2 ${⊢}\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)\to {F}\left({X}\right)\in {U}$
53 52 adantl ${⊢}\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 {F}\left({X}\right)\in {U}$
54 3 4 7 8 9 invginvrid
55 46 51 53 54 syl3anc
56 55 oveq1d
57 17 43 56 3eqtrd ${⊢}\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}$