Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  madjusmdetlem4 Structured version   Visualization version   GIF version

 Description: Lemma for madjusmdet 29225. (Contributed by Thierry Arnoux, 22-Aug-2020.)
Hypotheses
Ref Expression
madjusmdet.a 𝐴 = ((1...𝑁) Mat 𝑅)
madjusmdetlem2.p 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
madjusmdetlem2.s 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖)))
madjusmdetlem4.q 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗𝐽, (𝑗 − 1), 𝑗)))
madjusmdetlem4.t 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗𝑁, (𝑗 − 1), 𝑗)))
Assertion
Ref Expression
madjusmdetlem4 (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
Distinct variable groups:   𝐵,𝑖,𝑗   𝑖,𝐼,𝑗   𝑖,𝐽,𝑗   𝑖,𝑀,𝑗   𝑖,𝑁,𝑗   𝑃,𝑖,𝑗   𝑄,𝑖,𝑗   𝑅,𝑖,𝑗   𝜑,𝑖,𝑗   𝑆,𝑖,𝑗   𝑇,𝑖,𝑗
Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐷(𝑖,𝑗)   · (𝑖,𝑗)   𝐸(𝑖,𝑗)   𝐾(𝑖,𝑗)   𝑍(𝑖,𝑗)

Dummy variables 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 madjusmdet.b . . 3 𝐵 = (Base‘𝐴)
2 madjusmdet.a . . 3 𝐴 = ((1...𝑁) Mat 𝑅)
5 madjusmdet.t . . 3 · = (.r𝑅)
6 madjusmdet.z . . 3 𝑍 = (ℤRHom‘𝑅)
7 madjusmdet.e . . 3 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)
8 madjusmdet.n . . 3 (𝜑𝑁 ∈ ℕ)
9 madjusmdet.r . . 3 (𝜑𝑅 ∈ CRing)
10 madjusmdet.i . . 3 (𝜑𝐼 ∈ (1...𝑁))
11 madjusmdet.j . . 3 (𝜑𝐽 ∈ (1...𝑁))
12 madjusmdet.m . . 3 (𝜑𝑀𝐵)
13 eqid 2610 . . 3 (Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁)))
14 eqid 2610 . . 3 (pmSgn‘(1...𝑁)) = (pmSgn‘(1...𝑁))
15 eqid 2610 . . 3 (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
16 fveq2 6103 . . . . 5 (𝑘 = 𝑖 → ((𝑃𝑆)‘𝑘) = ((𝑃𝑆)‘𝑖))
1716oveq1d 6564 . . . 4 (𝑘 = 𝑖 → (((𝑃𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑙)) = (((𝑃𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑙)))
18 fveq2 6103 . . . . 5 (𝑙 = 𝑗 → ((𝑄𝑇)‘𝑙) = ((𝑄𝑇)‘𝑗))
1918oveq2d 6565 . . . 4 (𝑙 = 𝑗 → (((𝑃𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑙)) = (((𝑃𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑗)))
2017, 19cbvmpt2v 6633 . . 3 (𝑘 ∈ (1...𝑁), 𝑙 ∈ (1...𝑁) ↦ (((𝑃𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑙))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑗)))
21 eqid 2610 . . . . . 6 (1...𝑁) = (1...𝑁)
22 madjusmdetlem2.p . . . . . 6 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
23 eqid 2610 . . . . . 6 (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
2421, 22, 23, 13fzto1st 29184 . . . . 5 (𝐼 ∈ (1...𝑁) → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
2510, 24syl 17 . . . 4 (𝜑𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
26 nnuz 11599 . . . . . . . . 9 ℕ = (ℤ‘1)
278, 26syl6eleq 2698 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
28 eluzfz2 12220 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2927, 28syl 17 . . . . . . 7 (𝜑𝑁 ∈ (1...𝑁))
30 madjusmdetlem2.s . . . . . . . 8 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖)))
3121, 30, 23, 13fzto1st 29184 . . . . . . 7 (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
3229, 31syl 17 . . . . . 6 (𝜑𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
33 eqid 2610 . . . . . . 7 (invg‘(SymGrp‘(1...𝑁))) = (invg‘(SymGrp‘(1...𝑁)))
3423, 13, 33symginv 17645 . . . . . 6 (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((invg‘(SymGrp‘(1...𝑁)))‘𝑆) = 𝑆)
3532, 34syl 17 . . . . 5 (𝜑 → ((invg‘(SymGrp‘(1...𝑁)))‘𝑆) = 𝑆)
36 fzfid 12634 . . . . . . 7 (𝜑 → (1...𝑁) ∈ Fin)
3723symggrp 17643 . . . . . . 7 ((1...𝑁) ∈ Fin → (SymGrp‘(1...𝑁)) ∈ Grp)
3836, 37syl 17 . . . . . 6 (𝜑 → (SymGrp‘(1...𝑁)) ∈ Grp)
3913, 33grpinvcl 17290 . . . . . 6 (((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((invg‘(SymGrp‘(1...𝑁)))‘𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
4038, 32, 39syl2anc 691 . . . . 5 (𝜑 → ((invg‘(SymGrp‘(1...𝑁)))‘𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
4135, 40eqeltrrd 2689 . . . 4 (𝜑𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
42 eqid 2610 . . . . . 6 (+g‘(SymGrp‘(1...𝑁))) = (+g‘(SymGrp‘(1...𝑁)))
4323, 13, 42symgov 17633 . . . . 5 ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+g‘(SymGrp‘(1...𝑁)))𝑆) = (𝑃𝑆))
4423, 13, 42symgcl 17634 . . . . 5 ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+g‘(SymGrp‘(1...𝑁)))𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
4543, 44eqeltrrd 2689 . . . 4 ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
4625, 41, 45syl2anc 691 . . 3 (𝜑 → (𝑃𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
47 madjusmdetlem4.q . . . . . 6 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗𝐽, (𝑗 − 1), 𝑗)))
4821, 47, 23, 13fzto1st 29184 . . . . 5 (𝐽 ∈ (1...𝑁) → 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))))
4911, 48syl 17 . . . 4 (𝜑𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))))
50 madjusmdetlem4.t . . . . . . . 8 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗𝑁, (𝑗 − 1), 𝑗)))
5121, 50, 23, 13fzto1st 29184 . . . . . . 7 (𝑁 ∈ (1...𝑁) → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
5229, 51syl 17 . . . . . 6 (𝜑𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
5323, 13, 33symginv 17645 . . . . . 6 (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((invg‘(SymGrp‘(1...𝑁)))‘𝑇) = 𝑇)
5452, 53syl 17 . . . . 5 (𝜑 → ((invg‘(SymGrp‘(1...𝑁)))‘𝑇) = 𝑇)
5513, 33grpinvcl 17290 . . . . . 6 (((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((invg‘(SymGrp‘(1...𝑁)))‘𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
5638, 52, 55syl2anc 691 . . . . 5 (𝜑 → ((invg‘(SymGrp‘(1...𝑁)))‘𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
5754, 56eqeltrrd 2689 . . . 4 (𝜑𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
5823, 13, 42symgov 17633 . . . . 5 ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+g‘(SymGrp‘(1...𝑁)))𝑇) = (𝑄𝑇))
5923, 13, 42symgcl 17634 . . . . 5 ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+g‘(SymGrp‘(1...𝑁)))𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
6058, 59eqeltrrd 2689 . . . 4 ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
6149, 57, 60syl2anc 691 . . 3 (𝜑 → (𝑄𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
6223, 13symgbasf1o 17626 . . . . . . 7 (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
6332, 62syl 17 . . . . . 6 (𝜑𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
64 f1of1 6049 . . . . . 6 (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑆:(1...𝑁)–1-1→(1...𝑁))
65 df-f1 5809 . . . . . . 7 (𝑆:(1...𝑁)–1-1→(1...𝑁) ↔ (𝑆:(1...𝑁)⟶(1...𝑁) ∧ Fun 𝑆))
6665simprbi 479 . . . . . 6 (𝑆:(1...𝑁)–1-1→(1...𝑁) → Fun 𝑆)
6763, 64, 663syl 18 . . . . 5 (𝜑 → Fun 𝑆)
68 f1ocnv 6062 . . . . . . 7 (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
69 f1odm 6054 . . . . . . 7 (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → dom 𝑆 = (1...𝑁))
7063, 68, 693syl 18 . . . . . 6 (𝜑 → dom 𝑆 = (1...𝑁))
7129, 70eleqtrrd 2691 . . . . 5 (𝜑𝑁 ∈ dom 𝑆)
72 fvco 6184 . . . . 5 ((Fun 𝑆𝑁 ∈ dom 𝑆) → ((𝑃𝑆)‘𝑁) = (𝑃‘(𝑆𝑁)))
7367, 71, 72syl2anc 691 . . . 4 (𝜑 → ((𝑃𝑆)‘𝑁) = (𝑃‘(𝑆𝑁)))
7421, 30, 23, 13fzto1stinvn 29185 . . . . . 6 (𝑁 ∈ (1...𝑁) → (𝑆𝑁) = 1)
7529, 74syl 17 . . . . 5 (𝜑 → (𝑆𝑁) = 1)
7675fveq2d 6107 . . . 4 (𝜑 → (𝑃‘(𝑆𝑁)) = (𝑃‘1))
7721, 22fzto1stfv1 29182 . . . . 5 (𝐼 ∈ (1...𝑁) → (𝑃‘1) = 𝐼)
7810, 77syl 17 . . . 4 (𝜑 → (𝑃‘1) = 𝐼)
7973, 76, 783eqtrd 2648 . . 3 (𝜑 → ((𝑃𝑆)‘𝑁) = 𝐼)
8023, 13symgbasf1o 17626 . . . . . . 7 (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
8152, 80syl 17 . . . . . 6 (𝜑𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
82 f1of1 6049 . . . . . 6 (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑇:(1...𝑁)–1-1→(1...𝑁))
83 df-f1 5809 . . . . . . 7 (𝑇:(1...𝑁)–1-1→(1...𝑁) ↔ (𝑇:(1...𝑁)⟶(1...𝑁) ∧ Fun 𝑇))
8483simprbi 479 . . . . . 6 (𝑇:(1...𝑁)–1-1→(1...𝑁) → Fun 𝑇)
8581, 82, 843syl 18 . . . . 5 (𝜑 → Fun 𝑇)
86 f1ocnv 6062 . . . . . . 7 (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
87 f1odm 6054 . . . . . . 7 (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → dom 𝑇 = (1...𝑁))
8881, 86, 873syl 18 . . . . . 6 (𝜑 → dom 𝑇 = (1...𝑁))
8929, 88eleqtrrd 2691 . . . . 5 (𝜑𝑁 ∈ dom 𝑇)
90 fvco 6184 . . . . 5 ((Fun 𝑇𝑁 ∈ dom 𝑇) → ((𝑄𝑇)‘𝑁) = (𝑄‘(𝑇𝑁)))
9185, 89, 90syl2anc 691 . . . 4 (𝜑 → ((𝑄𝑇)‘𝑁) = (𝑄‘(𝑇𝑁)))
9221, 50, 23, 13fzto1stinvn 29185 . . . . . 6 (𝑁 ∈ (1...𝑁) → (𝑇𝑁) = 1)
9329, 92syl 17 . . . . 5 (𝜑 → (𝑇𝑁) = 1)
9493fveq2d 6107 . . . 4 (𝜑 → (𝑄‘(𝑇𝑁)) = (𝑄‘1))
9521, 47fzto1stfv1 29182 . . . . 5 (𝐽 ∈ (1...𝑁) → (𝑄‘1) = 𝐽)
9611, 95syl 17 . . . 4 (𝜑 → (𝑄‘1) = 𝐽)
9791, 94, 963eqtrd 2648 . . 3 (𝜑 → ((𝑄𝑇)‘𝑁) = 𝐽)
98 crngring 18381 . . . . . 6 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
999, 98syl 17 . . . . 5 (𝜑𝑅 ∈ Ring)
1002, 1minmar1cl 20276 . . . . 5 (((𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
10199, 12, 10, 11, 100syl22anc 1319 . . . 4 (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
1021, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 22, 30, 47, 50, 20, 101madjusmdetlem3 29223 . . 3 (𝜑 → (𝐼(subMat1‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))𝐽) = (𝑁(subMat1‘(𝑘 ∈ (1...𝑁), 𝑙 ∈ (1...𝑁) ↦ (((𝑃𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄𝑇)‘𝑙))))𝑁))
1031, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 20, 46, 61, 79, 97, 102madjusmdetlem1 29221 . 2 (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
10423, 14, 13psgnco 19748 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑃𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘𝑆)))
10536, 25, 41, 104syl3anc 1318 . . . . . . 7 (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘𝑆)))
10621, 22, 23, 13, 14psgnfzto1st 29186 . . . . . . . . 9 (𝐼 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
10710, 106syl 17 . . . . . . . 8 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
10823, 14, 13psgninv 19747 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘𝑆) = ((pmSgn‘(1...𝑁))‘𝑆))
10936, 32, 108syl2anc 691 . . . . . . . . 9 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑆) = ((pmSgn‘(1...𝑁))‘𝑆))
11021, 30, 23, 13, 14psgnfzto1st 29186 . . . . . . . . . 10 (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
11129, 110syl 17 . . . . . . . . 9 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
112109, 111eqtrd 2644 . . . . . . . 8 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
113107, 112oveq12d 6567 . . . . . . 7 (𝜑 → (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘𝑆)) = ((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))))
114105, 113eqtrd 2644 . . . . . 6 (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃𝑆)) = ((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))))
11523, 14, 13psgnco 19748 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑄𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘𝑇)))
11636, 49, 57, 115syl3anc 1318 . . . . . . 7 (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘𝑇)))
11721, 47, 23, 13, 14psgnfzto1st 29186 . . . . . . . . 9 (𝐽 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
11811, 117syl 17 . . . . . . . 8 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
11923, 14, 13psgninv 19747 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘𝑇) = ((pmSgn‘(1...𝑁))‘𝑇))
12036, 52, 119syl2anc 691 . . . . . . . . 9 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑇) = ((pmSgn‘(1...𝑁))‘𝑇))
12121, 50, 23, 13, 14psgnfzto1st 29186 . . . . . . . . . 10 (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
12229, 121syl 17 . . . . . . . . 9 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
123120, 122eqtrd 2644 . . . . . . . 8 (𝜑 → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
124118, 123oveq12d 6567 . . . . . . 7 (𝜑 → (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘𝑇)) = ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1))))
125116, 124eqtrd 2644 . . . . . 6 (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄𝑇)) = ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1))))
126114, 125oveq12d 6567 . . . . 5 (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄𝑇))) = (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))))
127 1cnd 9935 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
128127negcld 10258 . . . . . . . 8 (𝜑 → -1 ∈ ℂ)
129 fz1ssnn 12243 . . . . . . . . . . 11 (1...𝑁) ⊆ ℕ
130129, 10sseldi 3566 . . . . . . . . . 10 (𝜑𝐼 ∈ ℕ)
131130nnnn0d 11228 . . . . . . . . 9 (𝜑𝐼 ∈ ℕ0)
132 1nn0 11185 . . . . . . . . . 10 1 ∈ ℕ0
133132a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℕ0)
134131, 133nn0addcld 11232 . . . . . . . 8 (𝜑 → (𝐼 + 1) ∈ ℕ0)
135128, 134expcld 12870 . . . . . . 7 (𝜑 → (-1↑(𝐼 + 1)) ∈ ℂ)
1368nnnn0d 11228 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
137136, 133nn0addcld 11232 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ ℕ0)
138128, 137expcld 12870 . . . . . . 7 (𝜑 → (-1↑(𝑁 + 1)) ∈ ℂ)
139129, 11sseldi 3566 . . . . . . . . . 10 (𝜑𝐽 ∈ ℕ)
140139nnnn0d 11228 . . . . . . . . 9 (𝜑𝐽 ∈ ℕ0)
141140, 133nn0addcld 11232 . . . . . . . 8 (𝜑 → (𝐽 + 1) ∈ ℕ0)
142128, 141expcld 12870 . . . . . . 7 (𝜑 → (-1↑(𝐽 + 1)) ∈ ℂ)
143135, 138, 142, 138mul4d 10127 . . . . . 6 (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))))
144128, 141, 134expaddd 12872 . . . . . . . 8 (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))))
145130nncnd 10913 . . . . . . . . . . . 12 (𝜑𝐼 ∈ ℂ)
146139nncnd 10913 . . . . . . . . . . . 12 (𝜑𝐽 ∈ ℂ)
147145, 127, 146, 127add4d 10143 . . . . . . . . . . 11 (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + (1 + 1)))
148 1p1e2 11011 . . . . . . . . . . . 12 (1 + 1) = 2
149148oveq2i 6560 . . . . . . . . . . 11 ((𝐼 + 𝐽) + (1 + 1)) = ((𝐼 + 𝐽) + 2)
150147, 149syl6eq 2660 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + 2))
151150oveq2d 6565 . . . . . . . . 9 (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑((𝐼 + 𝐽) + 2)))
152 2nn0 11186 . . . . . . . . . . . 12 2 ∈ ℕ0
153152a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ0)
154131, 140nn0addcld 11232 . . . . . . . . . . 11 (𝜑 → (𝐼 + 𝐽) ∈ ℕ0)
155128, 153, 154expaddd 12872 . . . . . . . . . 10 (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · (-1↑2)))
156 neg1sqe1 12821 . . . . . . . . . . 11 (-1↑2) = 1
157156oveq2i 6560 . . . . . . . . . 10 ((-1↑(𝐼 + 𝐽)) · (-1↑2)) = ((-1↑(𝐼 + 𝐽)) · 1)
158155, 157syl6eq 2660 . . . . . . . . 9 (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · 1))
159128, 154expcld 12870 . . . . . . . . . 10 (𝜑 → (-1↑(𝐼 + 𝐽)) ∈ ℂ)
160159mulid1d 9936 . . . . . . . . 9 (𝜑 → ((-1↑(𝐼 + 𝐽)) · 1) = (-1↑(𝐼 + 𝐽)))
161151, 158, 1603eqtrd 2648 . . . . . . . 8 (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑(𝐼 + 𝐽)))
162144, 161eqtr3d 2646 . . . . . . 7 (𝜑 → ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) = (-1↑(𝐼 + 𝐽)))
163137nn0zd 11356 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ ℤ)
164 m1expcl2 12744 . . . . . . . 8 ((𝑁 + 1) ∈ ℤ → (-1↑(𝑁 + 1)) ∈ {-1, 1})
165 1neg1t1neg1 28902 . . . . . . . 8 ((-1↑(𝑁 + 1)) ∈ {-1, 1} → ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1))) = 1)
166163, 164, 1653syl 18 . . . . . . 7 (𝜑 → ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1))) = 1)
167162, 166oveq12d 6567 . . . . . 6 (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))) = ((-1↑(𝐼 + 𝐽)) · 1))
168143, 167, 1603eqtrd 2648 . . . . 5 (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (-1↑(𝐼 + 𝐽)))
169126, 168eqtrd 2644 . . . 4 (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄𝑇))) = (-1↑(𝐼 + 𝐽)))
170169fveq2d 6107 . . 3 (𝜑 → (𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄𝑇)))) = (𝑍‘(-1↑(𝐼 + 𝐽))))
171170oveq1d 6564 . 2 (𝜑 → ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
172103, 171eqtrd 2644 1 (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))