Theorem madjusmdetlem1 34529

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

Hypotheses

Ref	Expression
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	⊢ (𝜑 → 𝑀 ∈ 𝐵)
madjusmdetlem1.g	⊢ 𝐺 = (Base‘(SymGrp‘(1...𝑁)))
madjusmdetlem1.s	⊢ 𝑆 = (pmSgn‘(1...𝑁))
madjusmdetlem1.u	⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
madjusmdetlem1.w	⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)))
madjusmdetlem1.p	⊢ (𝜑 → 𝑃 ∈ 𝐺)
madjusmdetlem1.q	⊢ (𝜑 → 𝑄 ∈ 𝐺)
madjusmdetlem1.1	⊢ (𝜑 → (𝑃‘𝑁) = 𝐼)
madjusmdetlem1.2	⊢ (𝜑 → (𝑄‘𝑁) = 𝐽)
madjusmdetlem1.3	⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))

Assertion

Ref	Expression
madjusmdetlem1	⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Distinct variable groups:   𝐵,𝑖,𝑗   𝑖,𝐼,𝑗   𝑖,𝐽,𝑗   𝑖,𝑀,𝑗   𝑖,𝑁,𝑗   𝑃,𝑖,𝑗   𝑄,𝑖,𝑗   𝑅,𝑖,𝑗   𝜑,𝑖,𝑗   𝑖,𝐺,𝑗   𝑖,𝑊,𝑗   𝑈,𝑖,𝑗

Allowed substitution hints:   𝐴(𝑖, 𝑗)   𝐷(𝑖, 𝑗)   𝑆(𝑖, 𝑗)   · (𝑖, 𝑗)   𝐸(𝑖, 𝑗)   𝐾(𝑖, 𝑗)   𝑍(𝑖, 𝑗)

Proof of Theorem madjusmdetlem1

Step	Hyp	Ref	Expression
1		madjusmdet.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ 𝐵)
2		madjusmdet.j	. . . 4 ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))
3		madjusmdet.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))
4		madjusmdet.a	. . . . 5 ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)
5		madjusmdet.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐴)
6		madjusmdet.d	. . . . 5 ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)
7		madjusmdet.k	. . . . 5 ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)
8	4, 5, 6, 7	maducoevalmin1 22997	. . . 4 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐽 ∈ (1...𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
9	1, 2, 3, 8	syl3anc 1399	. . 3 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
10		madjusmdetlem1.u	. . . 4 ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
11	10	fveq2i 6911	. . 3 ⊢ (𝐷‘𝑈) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))
12	9, 11	eqtr4di 2816	. 2 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘𝑈))
13		madjusmdetlem1.g	. . 3 ⊢ 𝐺 = (Base‘(SymGrp‘(1...𝑁)))
14		madjusmdetlem1.s	. . 3 ⊢ 𝑆 = (pmSgn‘(1...𝑁))
15		madjusmdet.z	. . 3 ⊢ 𝑍 = (ℤRHom‘𝑅)
16		madjusmdet.t	. . 3 ⊢ · = (.r‘𝑅)
17		madjusmdetlem1.w	. . 3 ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)))
18		madjusmdet.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ CRing)
19		fzfid 14143	. . 3 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
20		crngring 20502	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
21	18, 20	syl 18	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
22	4, 5	minmar1cl 22996	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
23	21, 1, 3, 2, 22	syl22anc 852	. . . 4 ⊢ (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
24	10, 23	eqeltrid 2868	. . 3 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
25		madjusmdetlem1.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝐺)
26		madjusmdetlem1.q	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝐺)
27	4, 5, 6, 13, 14, 15, 16, 17, 18, 19, 24, 25, 26	mdetpmtr12 34527	. 2 ⊢ (𝜑 → (𝐷‘𝑈) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)))
28		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑖 = 𝑁)
29	28	fveq2d 6912	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁))
30		madjusmdetlem1.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃‘𝑁) = 𝐼)
31	30	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑁) = 𝐼)
32	31	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼)
33	29, 32	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼)
34		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑗 = 𝑁)
35	34	fveq2d 6912	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = (𝑄‘𝑁))
36		madjusmdetlem1.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄‘𝑁) = 𝐽)
37	36	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑁) = 𝐽)
38	37	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑁) = 𝐽)
39	35, 38	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = 𝐽)
40	33, 39	oveq12d 7461	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽))
41	1	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑀 ∈ 𝐵)
42	41	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵)
43	3	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐼 ∈ (1...𝑁))
44	43	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁))
45	2	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐽 ∈ (1...𝑁))
46	45	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁))
47		eqid 2763	. . . . . . . . . . . . 13 ⊢ ((1...𝑁) minMatR1 𝑅) = ((1...𝑁) minMatR1 𝑅)
48		eqid 2763	. . . . . . . . . . . . 13 ⊢ (1r‘𝑅) = (1r‘𝑅)
49		eqid 2763	. . . . . . . . . . . . 13 ⊢ (0g‘𝑅) = (0g‘𝑅)
50	4, 5, 47, 48, 49	minmar1eval 22994	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)))
51	42, 44, 46, 44, 46, 50	syl122anc 1407	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)))
52		eqid 2763	. . . . . . . . . . . . . 14 ⊢ 𝐼 = 𝐼
53	52	iftruei 4492	. . . . . . . . . . . . 13 ⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅))
54		eqid 2763	. . . . . . . . . . . . . 14 ⊢ 𝐽 = 𝐽
55	54	iftruei 4492	. . . . . . . . . . . . 13 ⊢ if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅)
56	53, 55	eqtri 2786	. . . . . . . . . . . 12 ⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅)
57	56	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅))
58	40, 51, 57	3eqtrrd 2803	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (1r‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
59		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑖 = 𝑁)
60	59	fveq2d 6912	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁))
61	31	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼)
62	60, 61	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼)
63	62	oveq1d 7458	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
64	41	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵)
65	43	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁))
66	45	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁))
67	26	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄 ∈ 𝐺)
68		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
69		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
70	69, 13	symgfv 19624	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ 𝐺 ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁))
71	67, 68, 70	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁))
72	71	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑄‘𝑗) ∈ (1...𝑁))
73	4, 5, 47, 48, 49	minmar1eval 22994	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ (𝑄‘𝑗) ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))))
74	64, 65, 66, 65, 72, 73	syl122anc 1407	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))))
75	52	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 = 𝐼)
76	75	iftrued 4493	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)))
77		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (𝑄‘𝑗) = 𝐽)
78	77	fveq2d 6912	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = (◡𝑄‘𝐽))
79	69, 13	symgbasf1o 19619	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ 𝐺 → 𝑄:(1...𝑁)⟶1-1onto(1...𝑁))
80	67, 79	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄:(1...𝑁)⟶1-1onto(1...𝑁))
81	80	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑄:(1...𝑁)⟶1-1onto(1...𝑁))
82	68	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 ∈ (1...𝑁))
83		f1ocnvfv1 7307	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄:(1...𝑁)⟶1-1onto(1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗)
84	81, 82, 83	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗)
85	36	fveq2d 6912	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = (◡𝑄‘𝐽))
86	26, 79	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(1...𝑁)⟶1-1onto(1...𝑁))
87		madjusmdet.n	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑁 ∈ ℕ)
88		nnuz 13031	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
89	87, 88	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
90		eluzfz2 13692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
91	89, 90	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92		f1ocnvfv1 7307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄:(1...𝑁)⟶1-1onto(1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑁)) = 𝑁)
93	86, 91, 92	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = 𝑁)
94	85, 93	eqtr3d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡𝑄‘𝐽) = 𝑁)
95	94	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘𝐽) = 𝑁)
96	95	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘𝐽) = 𝑁)
97	78, 84, 96	3eqtr3d 2806	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 = 𝑁)
98	97	ex 418	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → ((𝑄‘𝑗) = 𝐽 → 𝑗 = 𝑁))
99	98	con3d 153	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → (¬ 𝑗 = 𝑁 → ¬ (𝑄‘𝑗) = 𝐽))
100	99	imp 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ¬ (𝑄‘𝑗) = 𝐽)
101	100	iffalsed 4496	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅))
102	76, 101	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = (0g‘𝑅))
103	63, 74, 102	3eqtrrd 2803	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (0g‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
104	58, 103	ifeqda 4522	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
105		simp2 1155	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
106	105	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑖 ∈ (1...𝑁))
107	68	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑗 ∈ (1...𝑁))
108		ovexd 7478	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V)
109	10	oveqi 7456	. . . . . . . . . . . . . 14 ⊢ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))
110	109	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
111	110	mpoeq3ia 7521	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
112	17, 111	eqtri 2786	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
113	112	ovmpt4g 7591	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
114	106, 107, 108, 113	syl3anc 1399	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
115	104, 114	ifeqda 4522	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
116	115	mpoeq3dva 7520	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))))
117		eqid 2763	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
118	25	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑃 ∈ 𝐺)
119	69, 13	symgfv 19624	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁))
120	118, 105, 119	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁))
121	24	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑈 ∈ 𝐵)
122	4, 117, 5, 120, 71, 121	matecld 22771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) ∈ (Base‘𝑅))
123	4, 117, 5, 19, 18, 122	matbas2d 22768	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) ∈ 𝐵)
124	17, 123	eqeltrid 2868	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ 𝐵)
125	117, 48	ringidcl 20524	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ (Base‘𝑅))
126	21, 125	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
127		eqid 2763	. . . . . . . . 9 ⊢ ((1...𝑁) matRRep 𝑅) = ((1...𝑁) matRRep 𝑅)
128	4, 5, 127, 49	marrepval 22907	. . . . . . . 8 ⊢ (((𝑊 ∈ 𝐵 ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ (𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))))
129	124, 126, 91, 91, 128	syl22anc 852	. . . . . . 7 ⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))))
130	112	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))))
131	116, 129, 130	3eqtr4d 2808	. . . . . 6 ⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = 𝑊)
132	131	fveq2d 6912	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐷‘𝑊))
133		eqid 2763	. . . . . . . . . . . 12 ⊢ ((1...𝑁) subMat 𝑅) = ((1...𝑁) subMat 𝑅)
134	4, 133, 5	submaval 22926	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
135	124, 91, 91, 134	syl3anc 1399	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
136		fzdif2 33452	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
137	89, 136	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
138		mpoeq12 7516	. . . . . . . . . . 11 ⊢ ((((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)) ∧ ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
139	137, 137, 138	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
140	135, 139	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
141		difssd 4076	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁))
142	137, 141	eqsstrrd 3948	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
143	4, 5	submabas 22923	. . . . . . . . . 10 ⊢ ((𝑊 ∈ 𝐵 ∧ (1...(𝑁 − 1)) ⊆ (1...𝑁)) → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
144	124, 142, 143	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
145	140, 144	eqeltrd 2864	. . . . . . . 8 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
146		madjusmdet.e	. . . . . . . . 9 ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)
147		eqid 2763	. . . . . . . . 9 ⊢ ((1...(𝑁 − 1)) Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅)
148		eqid 2763	. . . . . . . . 9 ⊢ (Base‘((1...(𝑁 − 1)) Mat 𝑅)) = (Base‘((1...(𝑁 − 1)) Mat 𝑅))
149	146, 147, 148, 117	mdetcl 22941	. . . . . . . 8 ⊢ ((𝑅 ∈ CRing ∧ (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅))
150	18, 145, 149	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅))
151	117, 16, 48	ringlidm 20528	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
152	21, 150, 151	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
153	4	fveq2i 6911	. . . . . . . . . . 11 ⊢ (Base‘𝐴) = (Base‘((1...𝑁) Mat 𝑅))
154	5, 153	eqtri 2786	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘((1...𝑁) Mat 𝑅))
155	124, 154	eleqtrdi 2874	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅)))
156		smadiadetr 23020	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅))) ∧ (𝑁 ∈ (1...𝑁) ∧ (1r‘𝑅) ∈ (Base‘𝑅))) → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
157	18, 155, 91, 126, 156	syl22anc 852	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
158	6	fveq1i 6909	. . . . . . . . 9 ⊢ (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁))
159	16	oveqi 7456	. . . . . . . . 9 ⊢ ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
160	158, 159	eqeq12i 2781	. . . . . . . 8 ⊢ ((𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) ↔ (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
161	157, 160	sylibr 237	. . . . . . 7 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
162	137	oveq1d 7458	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = ((1...(𝑁 − 1)) maDet 𝑅))
163	162, 146	eqtr4di 2816	. . . . . . . . 9 ⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = 𝐸)
164	163	fveq1d 6910	. . . . . . . 8 ⊢ (𝜑 → ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
165	164	oveq2d 7459	. . . . . . 7 ⊢ (𝜑 → ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
166	161, 165	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
167	4, 5	submat1n 34507	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
168	87, 124, 167	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
169	168	fveq2d 6912	. . . . . 6 ⊢ (𝜑 → (𝐸‘(𝑁(subMat1‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
170	152, 166, 169	3eqtr4d 2808	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
171	132, 170	eqtr3d 2800	. . . 4 ⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
172	4, 5, 87, 3, 2, 21, 1, 10	submatminr1 34512	. . . . . 6 ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝑈)𝐽))
173		madjusmdetlem1.3	. . . . . 6 ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
174	172, 173	eqtrd 2798	. . . . 5 ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
175	174	fveq2d 6912	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐼(subMat1‘𝑀)𝐽)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
176	171, 175	eqtr4d 2801	. . 3 ⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))
177	176	oveq2d 7459	. 2 ⊢ (𝜑 → ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
178	12, 27, 177	3eqtrd 2802	1 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048  ifcif 4485  {csn 4588  ^◡ccnv 5654  ⟶1-1ontowf1o 6557  ‘cfv 6558  (class class class)co 7443   ∈ cmpo 7445  1c1 11228   · cmul 11232   − cmin 11568  ℕcn 12362  ℤ_≥cuz 12992  ...cfz 13666  Basecbs 17416  ._rcmulr 17458  0_gc0g 17639  SymGrpcsymg 19613  pmSgncpsgn 19733  1_rcur 20437  Ringcrg 20489  CRingccrg 20490  ℤRHomczrh 21835   Mat cmat 22752   matRRep cmarrep 22901   subMat csubma 22921   maDet cmdat 22929   maAdju cmadu 22977   minMatR1 cminmar1 22978  subMat1csmat 34495

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304  ax-addf 11306  ax-mulf 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-xor 1542  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-ot 4862  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-of 7717  df-om 7902  df-1st 8025  df-2nd 8026  df-supp 8205  df-tpos 8271  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-2o 8505  df-er 8745  df-map 8877  df-pm 8878  df-ixp 8954  df-en 9002  df-dom 9003  df-sdom 9004  df-fin 9005  df-fsupp 9382  df-sup 9461  df-oi 9531  df-card 10047  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001  df-nn 12363  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438  df-9 12439  df-n0 12634  df-xnn0 12707  df-z 12721  df-dec 12842  df-uz 12993  df-rp 13148  df-fz 13667  df-fzo 13816  df-seq 14172  df-exp 14232  df-hash 14502  df-word 14686  df-lsw 14735  df-concat 14743  df-s1 14770  df-substr 14817  df-pfx 14849  df-splice 14927  df-reverse 14936  df-s2 15027  df-struct 17354  df-sets 17371  df-slot 17389  df-ndx 17401  df-base 17417  df-ress 17438  df-plusg 17470  df-mulr 17471  df-starv 17472  df-sca 17473  df-vsca 17474  df-ip 17475  df-tset 17476  df-ple 17477  df-ds 17479  df-unif 17480  df-hom 17481  df-cco 17482  df-0g 17641  df-gsum 17642  df-prds 17647  df-pws 17649  df-mre 17785  df-mrc 17786  df-acs 17788  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-mhm 19007  df-submnd 19008  df-efmnd 19094  df-grp 19176  df-minusg 19177  df-mulg 19307  df-subg 19362  df-ghm 19457  df-gim 19502  df-cntz 19561  df-oppg 19590  df-symg 19614  df-pmtr 19686  df-psgn 19735  df-cmn 20026  df-abl 20027  df-mgp 20391  df-rng 20405  df-ur 20438  df-ring 20491  df-cring 20492  df-oppr 20597  df-dvdsr 20617  df-unit 20618  df-invr 20648  df-dvr 20661  df-rhm 20732  df-subrng 20828  df-subrg 20852  df-drng 21012  df-sra 21478  df-rgmod 21479  df-cnfld 21709  df-zring 21783  df-zrh 21839  df-dsmm 22068  df-frlm 22083  df-mat 22753  df-marrep 22903  df-subma 22922  df-mdet 22930  df-madu 22979  df-minmar1 22980  df-smat 34496

This theorem is used by:  madjusmdetlem4  34532