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	sselid	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → 𝑖 ∈ ℕ )
44	42 29	sselid	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 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 ‘ 𝑊 ) 𝑁 ) )