Metamath Proof Explorer


Theorem mdetunilem8

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a A=NMatR
mdetuni.b B=BaseA
mdetuni.k K=BaseR
mdetuni.0g 0˙=0R
mdetuni.1r 1˙=1R
mdetuni.pg +˙=+R
mdetuni.tg ·˙=R
mdetuni.n φNFin
mdetuni.r φRRing
mdetuni.ff φD:BK
mdetuni.al φxByNzNyzwNyxw=zxwDx=0˙
mdetuni.li φxByBzBwNxw×N=yw×N+˙fzw×NxNw×N=yNw×NxNw×N=zNw×NDx=Dy+˙Dz
mdetuni.sc φxByKzBwNxw×N=w×N×y·˙fzw×NxNw×N=zNw×NDx=y·˙Dz
mdetunilem8.id φD1A=0˙
Assertion mdetunilem8 φE:NNDaN,bNifEa=b1˙0˙=0˙

Proof

Step Hyp Ref Expression
1 mdetuni.a A=NMatR
2 mdetuni.b B=BaseA
3 mdetuni.k K=BaseR
4 mdetuni.0g 0˙=0R
5 mdetuni.1r 1˙=1R
6 mdetuni.pg +˙=+R
7 mdetuni.tg ·˙=R
8 mdetuni.n φNFin
9 mdetuni.r φRRing
10 mdetuni.ff φD:BK
11 mdetuni.al φxByNzNyzwNyxw=zxwDx=0˙
12 mdetuni.li φxByBzBwNxw×N=yw×N+˙fzw×NxNw×N=yNw×NxNw×N=zNw×NDx=Dy+˙Dz
13 mdetuni.sc φxByKzBwNxw×N=w×N×y·˙fzw×NxNw×N=zNw×NDx=y·˙Dz
14 mdetunilem8.id φD1A=0˙
15 simpl φE:N1-1Nφ
16 enrefg NFinNN
17 8 16 syl φNN
18 f1finf1o NNNFinE:N1-1NE:N1-1 ontoN
19 17 8 18 syl2anc φE:N1-1NE:N1-1 ontoN
20 19 biimpa φE:N1-1NE:N1-1 ontoN
21 1 matring NFinRRingARing
22 8 9 21 syl2anc φARing
23 eqid 1A=1A
24 2 23 ringidcl ARing1AB
25 22 24 syl φ1AB
26 25 adantr φE:N1-1N1AB
27 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem7 φE:N1-1 ontoN1ABDaN,bNEa1Ab=ℤRHomRpmSgnNE·˙D1A
28 15 20 26 27 syl3anc φE:N1-1NDaN,bNEa1Ab=ℤRHomRpmSgnNE·˙D1A
29 8 adantr φE:N1-1NNFin
30 29 3ad2ant1 φE:N1-1NaNbNNFin
31 9 adantr φE:N1-1NRRing
32 31 3ad2ant1 φE:N1-1NaNbNRRing
33 simp1r φE:N1-1NaNbNE:N1-1N
34 f1f E:N1-1NE:NN
35 33 34 syl φE:N1-1NaNbNE:NN
36 simp2 φE:N1-1NaNbNaN
37 35 36 ffvelrnd φE:N1-1NaNbNEaN
38 simp3 φE:N1-1NaNbNbN
39 1 5 4 30 32 37 38 23 mat1ov φE:N1-1NaNbNEa1Ab=ifEa=b1˙0˙
40 39 mpoeq3dva φE:N1-1NaN,bNEa1Ab=aN,bNifEa=b1˙0˙
41 40 fveq2d φE:N1-1NDaN,bNEa1Ab=DaN,bNifEa=b1˙0˙
42 14 adantr φE:N1-1ND1A=0˙
43 42 oveq2d φE:N1-1NℤRHomRpmSgnNE·˙D1A=ℤRHomRpmSgnNE·˙0˙
44 zrhpsgnmhm RRingNFinℤRHomRpmSgnNSymGrpNMndHommulGrpR
45 9 8 44 syl2anc φℤRHomRpmSgnNSymGrpNMndHommulGrpR
46 eqid BaseSymGrpN=BaseSymGrpN
47 eqid mulGrpR=mulGrpR
48 47 3 mgpbas K=BasemulGrpR
49 46 48 mhmf ℤRHomRpmSgnNSymGrpNMndHommulGrpRℤRHomRpmSgnN:BaseSymGrpNK
50 45 49 syl φℤRHomRpmSgnN:BaseSymGrpNK
51 50 adantr φE:N1-1NℤRHomRpmSgnN:BaseSymGrpNK
52 eqid SymGrpN=SymGrpN
53 52 46 elsymgbas NFinEBaseSymGrpNE:N1-1 ontoN
54 29 53 syl φE:N1-1NEBaseSymGrpNE:N1-1 ontoN
55 20 54 mpbird φE:N1-1NEBaseSymGrpN
56 51 55 ffvelrnd φE:N1-1NℤRHomRpmSgnNEK
57 3 7 4 ringrz RRingℤRHomRpmSgnNEKℤRHomRpmSgnNE·˙0˙=0˙
58 31 56 57 syl2anc φE:N1-1NℤRHomRpmSgnNE·˙0˙=0˙
59 43 58 eqtrd φE:N1-1NℤRHomRpmSgnNE·˙D1A=0˙
60 28 41 59 3eqtr3d φE:N1-1NDaN,bNifEa=b1˙0˙=0˙
61 60 ex φE:N1-1NDaN,bNifEa=b1˙0˙=0˙
62 61 adantr φE:NNE:N1-1NDaN,bNifEa=b1˙0˙=0˙
63 dff13 E:N1-1NE:NNcNdNEc=Edc=d
64 ibar E:NNcNdNEc=Edc=dE:NNcNdNEc=Edc=d
65 64 adantl φE:NNcNdNEc=Edc=dE:NNcNdNEc=Edc=d
66 63 65 bitr4id φE:NNE:N1-1NcNdNEc=Edc=d
67 66 notbid φE:NN¬E:N1-1N¬cNdNEc=Edc=d
68 rexnal cN¬dNEc=Edc=d¬cNdNEc=Edc=d
69 rexnal dN¬Ec=Edc=d¬dNEc=Edc=d
70 df-ne cd¬c=d
71 70 anbi2i Ec=EdcdEc=Ed¬c=d
72 annim Ec=Ed¬c=d¬Ec=Edc=d
73 71 72 bitr2i ¬Ec=Edc=dEc=Edcd
74 73 rexbii dN¬Ec=Edc=ddNEc=Edcd
75 69 74 bitr3i ¬dNEc=Edc=ddNEc=Edcd
76 75 rexbii cN¬dNEc=Edc=dcNdNEc=Edcd
77 68 76 bitr3i ¬cNdNEc=Edc=dcNdNEc=Edcd
78 67 77 bitrdi φE:NN¬E:N1-1NcNdNEc=Edcd
79 simprrl φE:NNcNdNEc=EdcdEc=Ed
80 fveqeq2 a=cEa=bEc=b
81 80 ifbid a=cifEa=b1˙0˙=ifEc=b1˙0˙
82 iftrue a=cifa=cifEc=b1˙0˙ifa=difEd=b1˙0˙ifEa=b1˙0˙=ifEc=b1˙0˙
83 81 82 eqtr4d a=cifEa=b1˙0˙=ifa=cifEc=b1˙0˙ifa=difEd=b1˙0˙ifEa=b1˙0˙
84 fveqeq2 a=dEa=bEd=b
85 84 ifbid a=difEa=b1˙0˙=ifEd=b1˙0˙
86 iftrue a=difa=difEd=b1˙0˙ifEa=b1˙0˙=ifEd=b1˙0˙
87 85 86 eqtr4d a=difEa=b1˙0˙=ifa=difEd=b1˙0˙ifEa=b1˙0˙
88 iffalse ¬a=difa=difEd=b1˙0˙ifEa=b1˙0˙=ifEa=b1˙0˙
89 88 eqcomd ¬a=difEa=b1˙0˙=ifa=difEd=b1˙0˙ifEa=b1˙0˙
90 87 89 pm2.61i ifEa=b1˙0˙=ifa=difEd=b1˙0˙ifEa=b1˙0˙
91 iffalse ¬a=cifa=cifEc=b1˙0˙ifa=difEd=b1˙0˙ifEa=b1˙0˙=ifa=difEd=b1˙0˙ifEa=b1˙0˙
92 90 91 eqtr4id ¬a=cifEa=b1˙0˙=ifa=cifEc=b1˙0˙ifa=difEd=b1˙0˙ifEa=b1˙0˙
93 83 92 pm2.61i ifEa=b1˙0˙=ifa=cifEc=b1˙0˙ifa=difEd=b1˙0˙ifEa=b1˙0˙
94 eqeq1 Ed=EcEd=bEc=b
95 94 eqcoms Ec=EdEd=bEc=b
96 95 ifbid Ec=EdifEd=b1˙0˙=ifEc=b1˙0˙
97 96 ifeq1d Ec=Edifa=difEd=b1˙0˙ifEa=b1˙0˙=ifa=difEc=b1˙0˙ifEa=b1˙0˙
98 97 ifeq2d Ec=Edifa=cifEc=b1˙0˙ifa=difEd=b1˙0˙ifEa=b1˙0˙=ifa=cifEc=b1˙0˙ifa=difEc=b1˙0˙ifEa=b1˙0˙
99 93 98 eqtrid Ec=EdifEa=b1˙0˙=ifa=cifEc=b1˙0˙ifa=difEc=b1˙0˙ifEa=b1˙0˙
100 99 mpoeq3dv Ec=EdaN,bNifEa=b1˙0˙=aN,bNifa=cifEc=b1˙0˙ifa=difEc=b1˙0˙ifEa=b1˙0˙
101 100 fveq2d Ec=EdDaN,bNifEa=b1˙0˙=DaN,bNifa=cifEc=b1˙0˙ifa=difEc=b1˙0˙ifEa=b1˙0˙
102 79 101 syl φE:NNcNdNEc=EdcdDaN,bNifEa=b1˙0˙=DaN,bNifa=cifEc=b1˙0˙ifa=difEc=b1˙0˙ifEa=b1˙0˙
103 simpll φE:NNcNdNEc=Edcdφ
104 simprll φE:NNcNdNEc=EdcdcN
105 simprlr φE:NNcNdNEc=EdcddN
106 simprrr φE:NNcNdNEc=Edcdcd
107 104 105 106 3jca φE:NNcNdNEc=EdcdcNdNcd
108 3 5 ringidcl RRing1˙K
109 9 108 syl φ1˙K
110 3 4 ring0cl RRing0˙K
111 9 110 syl φ0˙K
112 109 111 ifcld φifEc=b1˙0˙K
113 112 ad3antrrr φE:NNcNdNEc=EdcdbNifEc=b1˙0˙K
114 simp1ll φE:NNcNdNEc=EdcdaNbNφ
115 109 111 ifcld φifEa=b1˙0˙K
116 114 115 syl φE:NNcNdNEc=EdcdaNbNifEa=b1˙0˙K
117 1 2 3 4 5 6 7 8 9 10 11 12 13 103 107 113 116 mdetunilem2 φE:NNcNdNEc=EdcdDaN,bNifa=cifEc=b1˙0˙ifa=difEc=b1˙0˙ifEa=b1˙0˙=0˙
118 102 117 eqtrd φE:NNcNdNEc=EdcdDaN,bNifEa=b1˙0˙=0˙
119 118 expr φE:NNcNdNEc=EdcdDaN,bNifEa=b1˙0˙=0˙
120 119 rexlimdvva φE:NNcNdNEc=EdcdDaN,bNifEa=b1˙0˙=0˙
121 78 120 sylbid φE:NN¬E:N1-1NDaN,bNifEa=b1˙0˙=0˙
122 62 121 pm2.61d φE:NNDaN,bNifEa=b1˙0˙=0˙