Metamath Proof Explorer

Theorem madjusmdetlem3

Description: Lemma for madjusmdet . (Contributed by Thierry Arnoux, 27-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 ) , 𝑗 ) ) )
madjusmdetlem3.w ⊢ 𝑊 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
madjusmdetlem3.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
Assertion madjusmdetlem3 ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑁 ( 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 madjusmdetlem3.w ⊢ 𝑊 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
18 madjusmdetlem3.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
19 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
20 8 19 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
21 fzdif2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
22 20 21 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
23 difss ⊢ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ⊆ ( 1 ... 𝑁 )
24 22 23 eqsstrrdi ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
26 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
27 25 26 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
29 25 28 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
30 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) ∈ V )
31 17 ovmpt4g ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ∧ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) ∈ V ) → ( 𝑖 𝑊 𝑗 ) = ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
32 27 29 30 31 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 𝑊 𝑗 ) = ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
33 26 28 ovresd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) 𝑗 ) = ( 𝑖 𝑊 𝑗 ) )
34 eqid ⊢ ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 )
35 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑁 ∈ ℕ )
36 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
37 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝐽 ∈ ( 1 ... 𝑁 ) )
38 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
39 2 38 1 matbas2i ⊢ ( 𝑈 ∈ 𝐵 → 𝑈 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
40 18 39 syl ⊢ ( 𝜑 → 𝑈 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑈 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
42 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
43 42 27 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ℕ )
44 42 29 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑗 ∈ ℕ )
45 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) )
46 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑗 < 𝐽 , 𝑗 , ( 𝑗 + 1 ) ) = if ( 𝑗 < 𝐽 , 𝑗 , ( 𝑗 + 1 ) ) )
47 34 35 35 36 37 41 43 44 45 46 smatlem ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) 𝑗 ) = ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) 𝑈 if ( 𝑗 < 𝐽 , 𝑗 , ( 𝑗 + 1 ) ) ) )
48 1 2 3 4 5 6 7 8 9 10 10 12 13 14 madjusmdetlem2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) )
49 26 48 syldan ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) = ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) )
50 1 2 3 4 5 6 7 8 9 11 11 12 15 16 madjusmdetlem2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → if ( 𝑗 < 𝐽 , 𝑗 , ( 𝑗 + 1 ) ) = ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) )
51 28 50 syldan ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → if ( 𝑗 < 𝐽 , 𝑗 , ( 𝑗 + 1 ) ) = ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) )
52 49 51 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( if ( 𝑖 < 𝐼 , 𝑖 , ( 𝑖 + 1 ) ) 𝑈 if ( 𝑗 < 𝐽 , 𝑗 , ( 𝑗 + 1 ) ) ) = ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
53 47 52 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) 𝑗 ) = ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) )
54 32 33 53 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑖 ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) 𝑗 ) = ( 𝑖 ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) 𝑗 ) )
55 54 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∀ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑖 ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) 𝑗 ) = ( 𝑖 ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) 𝑗 ) )
56 eqid ⊢ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
57 2 1 56 34 8 10 11 18 smatcl ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
58 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
59 eqid ⊢ ( 1 ... 𝑁 ) = ( 1 ... 𝑁 )
60 eqid ⊢ ( SymGrp ‘ ( 1 ... 𝑁 ) ) = ( SymGrp ‘ ( 1 ... 𝑁 ) )
61 eqid ⊢ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) = ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
62 59 13 60 61 fzto1st ⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
63 10 62 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
64 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
65 20 64 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
66 59 14 60 61 fzto1st ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
67 65 66 syl ⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
68 eqid ⊢ ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) = ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
69 60 61 68 symginv ⊢ ( 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) = ◡ 𝑆 )
70 67 69 syl ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) = ◡ 𝑆 )
71 60 symggrp ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp )
72 58 71 syl ⊢ ( 𝜑 → ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp )
73 61 68 grpinvcl ⊢ ( ( ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp ∧ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
74 72 67 73 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
75 70 74 eqeltrrd ⊢ ( 𝜑 → ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
76 eqid ⊢ ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) = ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
77 60 61 76 symgov ⊢ ( ( 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑃 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑆 ) = ( 𝑃 ∘ ◡ 𝑆 ) )
78 60 61 76 symgcl ⊢ ( ( 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑃 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
79 77 78 eqeltrrd ⊢ ( ( 𝑃 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑆 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑃 ∘ ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
80 63 75 79 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
81 80 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ∘ ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
82 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
83 60 61 symgfv ⊢ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑁 ) )
84 81 82 83 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑁 ) )
85 59 15 60 61 fzto1st ⊢ ( 𝐽 ∈ ( 1 ... 𝑁 ) → 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
86 11 85 syl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
87 59 16 60 61 fzto1st ⊢ ( 𝑁 ∈ ( 1 ... 𝑁 ) → 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
88 65 87 syl ⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
89 60 61 68 symginv ⊢ ( 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) = ◡ 𝑇 )
90 88 89 syl ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) = ◡ 𝑇 )
91 61 68 grpinvcl ⊢ ( ( ( SymGrp ‘ ( 1 ... 𝑁 ) ) ∈ Grp ∧ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
92 72 88 91 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ‘ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
93 90 92 eqeltrrd ⊢ ( 𝜑 → ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
94 60 61 76 symgov ⊢ ( ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑄 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑇 ) = ( 𝑄 ∘ ◡ 𝑇 ) )
95 60 61 76 symgcl ⊢ ( ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑄 ( +g ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
96 94 95 eqeltrrd ⊢ ( ( 𝑄 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ ◡ 𝑇 ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) → ( 𝑄 ∘ ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
97 86 93 96 syl2anc ⊢ ( 𝜑 → ( 𝑄 ∘ ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
98 97 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ∘ ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) )
99 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
100 60 61 symgfv ⊢ ( ( ( 𝑄 ∘ ◡ 𝑇 ) ∈ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) )
101 98 99 100 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) )
102 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑈 ∈ 𝐵 )
103 2 38 1 84 101 102 matecld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
104 2 38 1 58 9 103 matbas2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑖 ) 𝑈 ( ( 𝑄 ∘ ◡ 𝑇 ) ‘ 𝑗 ) ) ) ∈ 𝐵 )
105 17 104 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
106 2 1 submatres ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) = ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
107 8 105 106 syl2anc ⊢ ( 𝜑 → ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) = ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
108 eqid ⊢ ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) = ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 )
109 2 1 56 108 8 65 65 105 smatcl ⊢ ( 𝜑 → ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
110 107 109 eqeltrrd ⊢ ( 𝜑 → ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
111 eqid ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
112 111 56 eqmat ⊢ ( ( ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ∧ ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ) → ( ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∀ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑖 ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) 𝑗 ) = ( 𝑖 ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) 𝑗 ) ) )
113 57 110 112 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∀ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑖 ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) 𝑗 ) = ( 𝑖 ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) 𝑗 ) ) )
114 55 113 mpbird ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑊 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
115 114 107 eqtr4d ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) )