Metamath Proof Explorer


Theorem lincresunit3lem1

Description: Lemma 1 for lincresunit3 . (Contributed by AV, 17-May-2019)

Ref Expression
Hypotheses lincresunit.b B=BaseM
lincresunit.r R=ScalarM
lincresunit.e E=BaseR
lincresunit.u U=UnitR
lincresunit.0 0˙=0R
lincresunit.z Z=0M
lincresunit.n N=invgR
lincresunit.i I=invrR
lincresunit.t ·˙=R
lincresunit.g G=sSXINFX·˙Fs
Assertion lincresunit3lem1 S𝒫BMLModXSFESFXUzSXNFXMGzMz=FzMz

Proof

Step Hyp Ref Expression
1 lincresunit.b B=BaseM
2 lincresunit.r R=ScalarM
3 lincresunit.e E=BaseR
4 lincresunit.u U=UnitR
5 lincresunit.0 0˙=0R
6 lincresunit.z Z=0M
7 lincresunit.n N=invgR
8 lincresunit.i I=invrR
9 lincresunit.t ·˙=R
10 lincresunit.g G=sSXINFX·˙Fs
11 fveq2 s=zFs=Fz
12 11 oveq2d s=zINFX·˙Fs=INFX·˙Fz
13 simpr3 S𝒫BMLModXSFESFXUzSXzSX
14 ovexd S𝒫BMLModXSFESFXUzSXINFX·˙FzV
15 10 12 13 14 fvmptd3 S𝒫BMLModXSFESFXUzSXGz=INFX·˙Fz
16 15 oveq1d S𝒫BMLModXSFESFXUzSXGzMz=INFX·˙FzMz
17 16 oveq2d S𝒫BMLModXSFESFXUzSXNFXMGzMz=NFXMINFX·˙FzMz
18 simp2 S𝒫BMLModXSMLMod
19 18 adantr S𝒫BMLModXSFESFXUzSXMLMod
20 2 lmodfgrp MLModRGrp
21 20 3ad2ant2 S𝒫BMLModXSRGrp
22 3 4 unitcl FXUFXE
23 22 3ad2ant2 FESFXUzSXFXE
24 3 7 grpinvcl RGrpFXENFXE
25 21 23 24 syl2an S𝒫BMLModXSFESFXUzSXNFXE
26 3simpa FESFXUzSXFESFXU
27 26 anim2i S𝒫BMLModXSFESFXUzSXS𝒫BMLModXSFESFXU
28 eldifi zSXzS
29 28 3ad2ant3 FESFXUzSXzS
30 29 adantl S𝒫BMLModXSFESFXUzSXzS
31 1 2 3 4 5 6 7 8 9 10 lincresunitlem2 S𝒫BMLModXSFESFXUzSINFX·˙FzE
32 27 30 31 syl2anc S𝒫BMLModXSFESFXUzSXINFX·˙FzE
33 elpwi S𝒫BSB
34 33 sseld S𝒫BzSzB
35 28 34 syl5com zSXS𝒫BzB
36 35 3ad2ant3 FESFXUzSXS𝒫BzB
37 36 com12 S𝒫BFESFXUzSXzB
38 37 3ad2ant1 S𝒫BMLModXSFESFXUzSXzB
39 38 imp S𝒫BMLModXSFESFXUzSXzB
40 eqid M=M
41 1 2 40 3 9 lmodvsass MLModNFXEINFX·˙FzEzBNFX·˙INFX·˙FzMz=NFXMINFX·˙FzMz
42 41 eqcomd MLModNFXEINFX·˙FzEzBNFXMINFX·˙FzMz=NFX·˙INFX·˙FzMz
43 19 25 32 39 42 syl13anc S𝒫BMLModXSFESFXUzSXNFXMINFX·˙FzMz=NFX·˙INFX·˙FzMz
44 2 lmodring MLModRRing
45 44 3ad2ant2 S𝒫BMLModXSRRing
46 45 adantr S𝒫BMLModXSFESFXUzSXRRing
47 elmapi FESF:SE
48 ffvelrn F:SEzSFzE
49 47 28 48 syl2an FESzSXFzE
50 49 3adant2 FESFXUzSXFzE
51 50 adantl S𝒫BMLModXSFESFXUzSXFzE
52 simp2 FESFXUzSXFXU
53 52 adantl S𝒫BMLModXSFESFXUzSXFXU
54 3 4 7 8 9 invginvrid RRingFzEFXUNFX·˙INFX·˙Fz=Fz
55 46 51 53 54 syl3anc S𝒫BMLModXSFESFXUzSXNFX·˙INFX·˙Fz=Fz
56 55 oveq1d S𝒫BMLModXSFESFXUzSXNFX·˙INFX·˙FzMz=FzMz
57 17 43 56 3eqtrd S𝒫BMLModXSFESFXUzSXNFXMGzMz=FzMz