Metamath Proof Explorer

Theorem madjusmdetlem4

Description: Lemma for madjusmdet . (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses madjusmdet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madjusmdet.a ⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
madjusmdet.d ⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
madjusmdet.k ⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
madjusmdet.t ⊢ · = ( .r ‘ 𝑅 )
madjusmdet.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
madjusmdet.e ⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
madjusmdet.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
madjusmdet.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
madjusmdet.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
madjusmdet.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
madjusmdet.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
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 madjusmdetlem4 ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 madjusmdet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
2 madjusmdet.a ⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
3 madjusmdet.d ⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
4 madjusmdet.k ⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
5 madjusmdet.t ⊢ · = ( .r ‘ 𝑅 )
6 madjusmdet.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
7 madjusmdet.e ⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
8 madjusmdet.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 madjusmdet.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
10 madjusmdet.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
11 madjusmdet.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
12 madjusmdet.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
13 madjusmdetlem2.p ⊢ 𝑃 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
14 madjusmdetlem2.s ⊢ 𝑆 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝑁 , if ( 𝑖 ≤ 𝑁 , ( 𝑖 − 1 ) , 𝑖 ) ) )
15 madjusmdetlem4.q ⊢ 𝑄 = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑗 = 1 , 𝐽 , if ( 𝑗 ≤ 𝐽 , ( 𝑗 − 1 ) , 𝑗 ) ) )
16 madjusmdetlem4.t ⊢ 𝑇 = ( 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑗 = 1 , 𝑁 , if ( 𝑗 ≤ 𝑁 , ( 𝑗 − 1 ) , 𝑗 ) ) )
17 eqid ⊢ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) = ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
18 eqid ⊢ ( pmSgn ‘ ( 1 ... 𝑁 ) ) = ( pmSgn ‘ ( 1 ... 𝑁 ) )
19 eqid ⊢ ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) = ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 )
20 fveq2 ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑘 ) = ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) )
21 20 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑘 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑙 ) ) = ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑙 ) ) )
22 fveq2 ⊢ ( 𝑙 = 𝑗 → ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑙 ) = ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) )
23 22 oveq2d ⊢ ( 𝑙 = 𝑗 → ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑙 ) ) = ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
24 21 23 cbvmpov ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) , 𝑙 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑘 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑙 ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
25 eqid ⊢ ( 1 ... 𝑁 ) = ( 1 ... 𝑁 )
26 eqid ⊢ ( SymGrp ‘ ( 1 ... 𝑁 ) ) = ( SymGrp ‘ ( 1 ... 𝑁 ) )
27 25 13 26 17 fzto1st ⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
28 10 27 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
29 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
30 8 29 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
31 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
32 30 31 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
33 25 14 26 17 fzto1st ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
34 32 33 syl ⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
35 eqid ⊢ ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) = ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
36 26 17 35 symginv ⊢ ( 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) = ◡ 𝑆 )
37 34 36 syl ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) = ◡ 𝑆 )
38 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
39 26 symggrp ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp )
40 38 39 syl ⊢ ( 𝜑 → ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp )
41 17 35 grpinvcl ⊢ ( ( ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp ∧ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
42 40 34 41 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
43 37 42 eqeltrrd ⊢ ( 𝜑 → ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
44 eqid ⊢ ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) = ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
45 26 17 44 symgov ⊢ ( ( 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑃 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑆 ) = ( 𝑃 ∘ ◡ 𝑆 ) )
46 26 17 44 symgcl ⊢ ( ( 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑃 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
47 45 46 eqeltrrd ⊢ ( ( 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑃 ∘ ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
48 28 43 47 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
49 25 15 26 17 fzto1st ⊢ ( 𝐽 ∈ ( 1 ... 𝑁 ) → 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
50 11 49 syl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
51 25 16 26 17 fzto1st ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
52 32 51 syl ⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
53 26 17 35 symginv ⊢ ( 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) = ◡ 𝑇 )
54 52 53 syl ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) = ◡ 𝑇 )
55 17 35 grpinvcl ⊢ ( ( ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp ∧ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
56 40 52 55 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
57 54 56 eqeltrrd ⊢ ( 𝜑 → ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
58 26 17 44 symgov ⊢ ( ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑄 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑇 ) = ( 𝑄 ∘ ◡ 𝑇 ) )
59 26 17 44 symgcl ⊢ ( ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑄 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
60 58 59 eqeltrrd ⊢ ( ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑄 ∘ ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
61 50 57 60 syl2anc ⊢ ( 𝜑 → ( 𝑄 ∘ ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
62 26 17 symgbasf1o ⊢ ( 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) → 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
63 34 62 syl ⊢ ( 𝜑 → 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
64 f1of1 ⊢ ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑆 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
65 df-f1 ⊢ ( 𝑆 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ↔ ( 𝑆 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) ∧ Fun ◡ 𝑆 ) )
66 65 simprbi ⊢ ( 𝑆 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) → Fun ◡ 𝑆 )
67 63 64 66 3syl ⊢ ( 𝜑 → Fun ◡ 𝑆 )
68 f1ocnv ⊢ ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
69 f1odm ⊢ ( ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → dom ◡ 𝑆 = ( 1 ... 𝑁 ) )
70 63 68 69 3syl ⊢ ( 𝜑 → dom ◡ 𝑆 = ( 1 ... 𝑁 ) )
71 32 70 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom ◡ 𝑆 )
72 fvco ⊢ ( ( Fun ◡ 𝑆 ∧ 𝑁 ∈ dom ◡ 𝑆 ) → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑁 ) = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑁 ) ) )
73 67 71 72 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑁 ) = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑁 ) ) )
74 25 14 26 17 fzto1stinvn ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( ◡ 𝑆 ‘ 𝑁 ) = 1 )
75 32 74 syl ⊢ ( 𝜑 → ( ◡ 𝑆 ‘ 𝑁 ) = 1 )
76 75 fveq2d ⊢ ( 𝜑 → ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑁 ) ) = ( 𝑃 ‘ 1 ) )
77 25 13 fzto1stfv1 ⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → ( 𝑃 ‘ 1 ) = 𝐼 )
78 10 77 syl ⊢ ( 𝜑 → ( 𝑃 ‘ 1 ) = 𝐼 )
79 73 76 78 3eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑁 ) = 𝐼 )
80 26 17 symgbasf1o ⊢ ( 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) → 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
81 52 80 syl ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
82 f1of1 ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
83 df-f1 ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ↔ ( 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) ∧ Fun ◡ 𝑇 ) )
84 83 simprbi ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) → Fun ◡ 𝑇 )
85 81 82 84 3syl ⊢ ( 𝜑 → Fun ◡ 𝑇 )
86 f1ocnv ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ◡ 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
87 f1odm ⊢ ( ◡ 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → dom ◡ 𝑇 = ( 1 ... 𝑁 ) )
88 81 86 87 3syl ⊢ ( 𝜑 → dom ◡ 𝑇 = ( 1 ... 𝑁 ) )
89 32 88 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom ◡ 𝑇 )
90 fvco ⊢ ( ( Fun ◡ 𝑇 ∧ 𝑁 ∈ dom ◡ 𝑇 ) → ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑁 ) = ( 𝑄 ‘ ( ◡ 𝑇 ‘ 𝑁 ) ) )
91 85 89 90 syl2anc ⊢ ( 𝜑 → ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑁 ) = ( 𝑄 ‘ ( ◡ 𝑇 ‘ 𝑁 ) ) )
92 25 16 26 17 fzto1stinvn ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( ◡ 𝑇 ‘ 𝑁 ) = 1 )
93 32 92 syl ⊢ ( 𝜑 → ( ◡ 𝑇 ‘ 𝑁 ) = 1 )
94 93 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( ◡ 𝑇 ‘ 𝑁 ) ) = ( 𝑄 ‘ 1 ) )
95 25 15 fzto1stfv1 ⊢ ( 𝐽 ∈ ( 1 ... 𝑁 ) → ( 𝑄 ‘ 1 ) = 𝐽 )
96 11 95 syl ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) = 𝐽 )
97 91 94 96 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑁 ) = 𝐽 )
98 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
99 9 98 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
100 2 1 minmar1cl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ∈ 𝐵 )
101 99 12 10 11 100 syl22anc ⊢ ( 𝜑 → ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ∈ 𝐵 )
102 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 24 101 madjusmdetlem3 ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ) 𝐽 ) = ( 𝑁 ( subMat1 ‘ ( 𝑘 ∈ ( 1 ... 𝑁 ) , 𝑙 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑘 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑙 ) ) ) ) 𝑁 ) )
103 1 2 3 4 5 6 7 8 9 10 11 12 17 18 19 24 48 61 79 97 102 madjusmdetlem1 ⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )
104 26 18 17 psgnco ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) = ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑃 ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑆 ) ) )
105 38 28 43 104 syl3anc ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) = ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑃 ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑆 ) ) )
106 25 13 26 17 18 psgnfzto1st ⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) )
107 10 106 syl ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑃 ) = ( - 1 ↑ ( 𝐼 + 1 ) ) )
108 26 18 17 psgninv ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑆 ) = ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑆 ) )
109 38 34 108 syl2anc ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑆 ) = ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑆 ) )
110 25 14 26 17 18 psgnfzto1st ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑆 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
111 32 110 syl ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑆 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
112 109 111 eqtrd ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑆 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
113 107 112 oveq12d ⊢ ( 𝜑 → ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑃 ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑆 ) ) = ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) )
114 105 113 eqtrd ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) = ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) )
115 26 18 17 psgnco ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) = ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑄 ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑇 ) ) )
116 38 50 57 115 syl3anc ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) = ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑄 ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑇 ) ) )
117 25 15 26 17 18 psgnfzto1st ⊢ ( 𝐽 ∈ ( 1 ... 𝑁 ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑄 ) = ( - 1 ↑ ( 𝐽 + 1 ) ) )
118 11 117 syl ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑄 ) = ( - 1 ↑ ( 𝐽 + 1 ) ) )
119 26 18 17 psgninv ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑇 ) = ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑇 ) )
120 38 52 119 syl2anc ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑇 ) = ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑇 ) )
121 25 16 26 17 18 psgnfzto1st ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑇 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
122 32 121 syl ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑇 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
123 120 122 eqtrd ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑇 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
124 118 123 oveq12d ⊢ ( 𝜑 → ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ 𝑄 ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ◡ 𝑇 ) ) = ( ( - 1 ↑ ( 𝐽 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) )
125 116 124 eqtrd ⊢ ( 𝜑 → ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) = ( ( - 1 ↑ ( 𝐽 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) )
126 114 125 oveq12d ⊢ ( 𝜑 → ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) ) = ( ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) · ( ( - 1 ↑ ( 𝐽 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) ) )
127 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
128 127 negcld ⊢ ( 𝜑 → - 1 ∈ ℂ )
129 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
130 129 10 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
131 130 nnnn0d ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
132 1nn0 ⊢ 1 ∈ ℕ0
133 132 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
134 131 133 nn0addcld ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℕ0 )
135 128 134 expcld ⊢ ( 𝜑 → ( - 1 ↑ ( 𝐼 + 1 ) ) ∈ ℂ )
136 8 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
137 136 133 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
138 128 137 expcld ⊢ ( 𝜑 → ( - 1 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
139 129 11 sselid ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
140 139 nnnn0d ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
141 140 133 nn0addcld ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℕ0 )
142 128 141 expcld ⊢ ( 𝜑 → ( - 1 ↑ ( 𝐽 + 1 ) ) ∈ ℂ )
143 135 138 142 138 mul4d ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) · ( ( - 1 ↑ ( 𝐽 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) ) = ( ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝐽 + 1 ) ) ) · ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) ) )
144 128 141 134 expaddd ⊢ ( 𝜑 → ( - 1 ↑ ( ( 𝐼 + 1 ) + ( 𝐽 + 1 ) ) ) = ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝐽 + 1 ) ) ) )
145 130 nncnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
146 139 nncnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
147 145 127 146 127 add4d ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) + ( 𝐽 + 1 ) ) = ( ( 𝐼 + 𝐽 ) + ( 1 + 1 ) ) )
148 1p1e2 ⊢ ( 1 + 1 ) = 2
149 148 oveq2i ⊢ ( ( 𝐼 + 𝐽 ) + ( 1 + 1 ) ) = ( ( 𝐼 + 𝐽 ) + 2 )
150 147 149 eqtrdi ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) + ( 𝐽 + 1 ) ) = ( ( 𝐼 + 𝐽 ) + 2 ) )
151 150 oveq2d ⊢ ( 𝜑 → ( - 1 ↑ ( ( 𝐼 + 1 ) + ( 𝐽 + 1 ) ) ) = ( - 1 ↑ ( ( 𝐼 + 𝐽 ) + 2 ) ) )
152 2nn0 ⊢ 2 ∈ ℕ0
153 152 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
154 131 140 nn0addcld ⊢ ( 𝜑 → ( 𝐼 + 𝐽 ) ∈ ℕ0 )
155 128 153 154 expaddd ⊢ ( 𝜑 → ( - 1 ↑ ( ( 𝐼 + 𝐽 ) + 2 ) ) = ( ( - 1 ↑ ( 𝐼 + 𝐽 ) ) · ( - 1 ↑ 2 ) ) )
156 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
157 156 oveq2i ⊢ ( ( - 1 ↑ ( 𝐼 + 𝐽 ) ) · ( - 1 ↑ 2 ) ) = ( ( - 1 ↑ ( 𝐼 + 𝐽 ) ) · 1 )
158 155 157 eqtrdi ⊢ ( 𝜑 → ( - 1 ↑ ( ( 𝐼 + 𝐽 ) + 2 ) ) = ( ( - 1 ↑ ( 𝐼 + 𝐽 ) ) · 1 ) )
159 128 154 expcld ⊢ ( 𝜑 → ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ∈ ℂ )
160 159 mulridd ⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝐼 + 𝐽 ) ) · 1 ) = ( - 1 ↑ ( 𝐼 + 𝐽 ) ) )
161 151 158 160 3eqtrd ⊢ ( 𝜑 → ( - 1 ↑ ( ( 𝐼 + 1 ) + ( 𝐽 + 1 ) ) ) = ( - 1 ↑ ( 𝐼 + 𝐽 ) ) )
162 144 161 eqtr3d ⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝐽 + 1 ) ) ) = ( - 1 ↑ ( 𝐼 + 𝐽 ) ) )
163 137 nn0zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
164 m1expcl2 ⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( - 1 ↑ ( 𝑁 + 1 ) ) ∈ { - 1 , 1 } )
165 1neg1t1neg1 ⊢ ( ( - 1 ↑ ( 𝑁 + 1 ) ) ∈ { - 1 , 1 } → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) = 1 )
166 163 164 165 3syl ⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) = 1 )
167 162 166 oveq12d ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝐽 + 1 ) ) ) · ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) ) = ( ( - 1 ↑ ( 𝐼 + 𝐽 ) ) · 1 ) )
168 143 167 160 3eqtrd ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝐼 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) · ( ( - 1 ↑ ( 𝐽 + 1 ) ) · ( - 1 ↑ ( 𝑁 + 1 ) ) ) ) = ( - 1 ↑ ( 𝐼 + 𝐽 ) ) )
169 126 168 eqtrd ⊢ ( 𝜑 → ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) ) = ( - 1 ↑ ( 𝐼 + 𝐽 ) ) )
170 169 fveq2d ⊢ ( 𝜑 → ( 𝑍 ‘ ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) ) ) = ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ) )
171 170 oveq1d ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑃 ∘ ◡ 𝑆 ) ) · ( ( pmSgn ‘ ( 1 ... 𝑁 ) ) ‘ ( 𝑄 ∘ ◡ 𝑇 ) ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )
172 103 171 eqtrd ⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( - 1 ↑ ( 𝐼 + 𝐽 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )