Metamath Proof Explorer


Theorem zlmodzxzldeplem3

Description: Lemma 3 for zlmodzxzldep . (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z Z=ringfreeLMod01
zlmodzxzldep.a A=0316
zlmodzxzldep.b B=0214
zlmodzxzldeplem.f F=A2B3
Assertion zlmodzxzldeplem3 FlinCZAB=0Z

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z Z=ringfreeLMod01
2 zlmodzxzldep.a A=0316
3 zlmodzxzldep.b B=0214
4 zlmodzxzldeplem.f F=A2B3
5 ovex ringfreeLMod01V
6 1 5 eqeltri ZV
7 1 2 3 4 zlmodzxzldeplem1 FAB
8 1 zlmodzxzlmod ZLModring=ScalarZ
9 simpr ZLModring=ScalarZring=ScalarZ
10 9 eqcomd ZLModring=ScalarZScalarZ=ring
11 8 10 ax-mp ScalarZ=ring
12 11 fveq2i BaseScalarZ=Basering
13 zringbas =Basering
14 13 eqcomi Basering=
15 12 14 eqtri BaseScalarZ=
16 15 oveq1i BaseScalarZAB=AB
17 7 16 eleqtrri FBaseScalarZAB
18 3z 3
19 6nn 6
20 19 nnzi 6
21 1 zlmodzxzel 360316BaseZ
22 18 20 21 mp2an 0316BaseZ
23 2z 2
24 4z 4
25 1 zlmodzxzel 240214BaseZ
26 23 24 25 mp2an 0214BaseZ
27 2 eleq1i ABaseZ0316BaseZ
28 3 eleq1i BBaseZ0214BaseZ
29 27 28 anbi12i ABaseZBBaseZ0316BaseZ0214BaseZ
30 22 26 29 mpbir2an ABaseZBBaseZ
31 prelpwi ABaseZBBaseZAB𝒫BaseZ
32 30 31 ax-mp AB𝒫BaseZ
33 lincval ZVFBaseScalarZABAB𝒫BaseZFlinCZAB=ZxABFxZx
34 6 17 32 33 mp3an FlinCZAB=ZxABFxZx
35 lmodcmn ZLModZCMnd
36 35 adantr ZLModring=ScalarZZCMnd
37 8 36 ax-mp ZCMnd
38 prex 0316V
39 2 38 eqeltri AV
40 prex 0214V
41 3 40 eqeltri BV
42 1 2 3 zlmodzxzldeplem AB
43 39 41 42 3pm3.2i AVBVAB
44 8 simpli ZLMod
45 elmapi FABF:AB
46 39 prid1 AAB
47 ffvelrn F:ABAABFA
48 46 47 mpan2 F:ABFA
49 7 45 48 mp2b FA
50 8 9 ax-mp ring=ScalarZ
51 50 eqcomi ScalarZ=ring
52 51 fveq2i BaseScalarZ=Basering
53 52 14 eqtri BaseScalarZ=
54 49 53 eleqtrri FABaseScalarZ
55 2 22 eqeltri ABaseZ
56 eqid BaseZ=BaseZ
57 eqid ScalarZ=ScalarZ
58 eqid Z=Z
59 eqid BaseScalarZ=BaseScalarZ
60 56 57 58 59 lmodvscl ZLModFABaseScalarZABaseZFAZABaseZ
61 44 54 55 60 mp3an FAZABaseZ
62 41 prid2 BAB
63 ffvelrn F:ABBABFB
64 62 63 mpan2 F:ABFB
65 7 45 64 mp2b FB
66 65 53 eleqtrri FBBaseScalarZ
67 3 26 eqeltri BBaseZ
68 56 57 58 59 lmodvscl ZLModFBBaseScalarZBBaseZFBZBBaseZ
69 44 66 67 68 mp3an FBZBBaseZ
70 61 69 pm3.2i FAZABaseZFBZBBaseZ
71 eqid +Z=+Z
72 fveq2 x=AFx=FA
73 id x=Ax=A
74 72 73 oveq12d x=AFxZx=FAZA
75 fveq2 x=BFx=FB
76 id x=Bx=B
77 75 76 oveq12d x=BFxZx=FBZB
78 56 71 74 77 gsumpr ZCMndAVBVABFAZABaseZFBZBBaseZZxABFxZx=FAZA+ZFBZB
79 37 43 70 78 mp3an ZxABFxZx=FAZA+ZFBZB
80 4 fveq1i FA=A2B3A
81 2ex 2V
82 39 81 fvpr1 ABA2B3A=2
83 42 82 ax-mp A2B3A=2
84 80 83 eqtri FA=2
85 84 oveq1i FAZA=2ZA
86 4 fveq1i FB=A2B3B
87 negex 3V
88 41 87 fvpr2 ABA2B3B=3
89 42 88 ax-mp A2B3B=3
90 86 89 eqtri FB=3
91 90 oveq1i FBZB=-3ZB
92 85 91 oveq12i FAZA+ZFBZB=2ZA+Z-3ZB
93 eqid 0010=0010
94 1 93 zlmodzxz0 0010=0Z
95 94 eqcomi 0Z=0010
96 1 2 3 95 71 58 zlmodzxzequap 2ZA+Z-3ZB=0Z
97 92 96 eqtri FAZA+ZFBZB=0Z
98 34 79 97 3eqtri FlinCZAB=0Z