Theorem madjusmdetlem1 33971

Description: Lemma for madjusmdet 33975. (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 22617	. . . 4 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐽 ∈ (1...𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
9	1, 2, 3, 8	syl3anc 1374	. . 3 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
10		madjusmdetlem1.u	. . . 4 ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
11	10	fveq2i 6844	. . 3 ⊢ (𝐷‘𝑈) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))
12	9, 11	eqtr4di 2790	. 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 13935	. . 3 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
20		crngring 20226	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
21	18, 20	syl 17	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
22	4, 5	minmar1cl 22616	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
23	21, 1, 3, 2, 22	syl22anc 839	. . . 4 ⊢ (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
24	10, 23	eqeltrid 2841	. . 3 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
25		madjusmdetlem1.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝐺)
26		madjusmdetlem1.q	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝐺)
27	4, 5, 6, 13, 14, 15, 16, 17, 18, 19, 24, 25, 26	mdetpmtr12 33969	. 2 ⊢ (𝜑 → (𝐷‘𝑈) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)))
28		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑖 = 𝑁)
29	28	fveq2d 6845	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁))
30		madjusmdetlem1.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃‘𝑁) = 𝐼)
31	30	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑁) = 𝐼)
32	31	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼)
33	29, 32	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼)
34		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑗 = 𝑁)
35	34	fveq2d 6845	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = (𝑄‘𝑁))
36		madjusmdetlem1.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑄‘𝑁) = 𝐽)
37	36	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑁) = 𝐽)
38	37	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑁) = 𝐽)
39	35, 38	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄‘𝑗) = 𝐽)
40	33, 39	oveq12d 7385	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽))
41	1	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑀 ∈ 𝐵)
42	41	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵)
43	3	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐼 ∈ (1...𝑁))
44	43	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁))
45	2	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐽 ∈ (1...𝑁))
46	45	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁))
47		eqid 2737	. . . . . . . . . . . . 13 ⊢ ((1...𝑁) minMatR1 𝑅) = ((1...𝑁) minMatR1 𝑅)
48		eqid 2737	. . . . . . . . . . . . 13 ⊢ (1r‘𝑅) = (1r‘𝑅)
49		eqid 2737	. . . . . . . . . . . . 13 ⊢ (0g‘𝑅) = (0g‘𝑅)
50	4, 5, 47, 48, 49	minmar1eval 22614	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)))
51	42, 44, 46, 44, 46, 50	syl122anc 1382	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)))
52		eqid 2737	. . . . . . . . . . . . . 14 ⊢ 𝐼 = 𝐼
53	52	iftruei 4474	. . . . . . . . . . . . 13 ⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅))
54		eqid 2737	. . . . . . . . . . . . . 14 ⊢ 𝐽 = 𝐽
55	54	iftruei 4474	. . . . . . . . . . . . 13 ⊢ if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (1r‘𝑅)
56	53, 55	eqtri 2760	. . . . . . . . . . . 12 ⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅)
57	56	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = (1r‘𝑅))
58	40, 51, 57	3eqtrrd 2777	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (1r‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
59		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑖 = 𝑁)
60	59	fveq2d 6845	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁))
61	31	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼)
62	60, 61	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼)
63	62	oveq1d 7382	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
64	41	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑀 ∈ 𝐵)
65	43	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁))
66	45	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁))
67	26	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄 ∈ 𝐺)
68		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
69		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
70	69, 13	symgfv 19355	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ 𝐺 ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁))
71	67, 68, 70	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘𝑗) ∈ (1...𝑁))
72	71	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑄‘𝑗) ∈ (1...𝑁))
73	4, 5, 47, 48, 49	minmar1eval 22614	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ (𝑄‘𝑗) ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))))
74	64, 65, 66, 65, 72, 73	syl122anc 1382	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) = if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))))
75	52	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 = 𝐼)
76	75	iftrued 4475	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)))
77		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (𝑄‘𝑗) = 𝐽)
78	77	fveq2d 6845	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = (◡𝑄‘𝐽))
79	69, 13	symgbasf1o 19350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ 𝐺 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
80	67, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
81	80	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
82	68	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 ∈ (1...𝑁))
83		f1ocnvfv1 7231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗)
84	81, 82, 83	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗)
85	36	fveq2d 6845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = (◡𝑄‘𝐽))
86	26, 79	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
87		madjusmdet.n	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑁 ∈ ℕ)
88		nnuz 12827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
89	87, 88	eleqtrdi 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
90		eluzfz2 13486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92		f1ocnvfv1 7231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑁)) = 𝑁)
93	86, 91, 92	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = 𝑁)
94	85, 93	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡𝑄‘𝐽) = 𝑁)
95	94	3ad2ant1 1134	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘𝐽) = 𝑁)
96	95	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘𝐽) = 𝑁)
97	78, 84, 96	3eqtr3d 2780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → 𝑗 = 𝑁)
98	97	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → ((𝑄‘𝑗) = 𝐽 → 𝑗 = 𝑁))
99	98	con3d 152	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → (¬ 𝑗 = 𝑁 → ¬ (𝑄‘𝑗) = 𝐽))
100	99	imp 406	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ¬ (𝑄‘𝑗) = 𝐽)
101	100	iffalsed 4478	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅))
102	76, 101	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = (0g‘𝑅))
103	63, 74, 102	3eqtrrd 2777	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (0g‘𝑅) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
104	58, 103	ifeqda 4504	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
105		simp2 1138	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
106	105	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑖 ∈ (1...𝑁))
107	68	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑗 ∈ (1...𝑁))
108		ovexd 7402	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V)
109	10	oveqi 7380	. . . . . . . . . . . . . 14 ⊢ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))
110	109	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
111	110	mpoeq3ia 7445	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
112	17, 111	eqtri 2760	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
113	112	ovmpt4g 7514	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
114	106, 107, 108, 113	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
115	104, 114	ifeqda 4504	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
116	115	mpoeq3dva 7444	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))))
117		eqid 2737	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
118	25	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑃 ∈ 𝐺)
119	69, 13	symgfv 19355	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁))
120	118, 105, 119	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃‘𝑖) ∈ (1...𝑁))
121	24	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑈 ∈ 𝐵)
122	4, 117, 5, 120, 71, 121	matecld 22391	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) ∈ (Base‘𝑅))
123	4, 117, 5, 19, 18, 122	matbas2d 22388	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) ∈ 𝐵)
124	17, 123	eqeltrid 2841	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ 𝐵)
125	117, 48	ringidcl 20246	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ (Base‘𝑅))
126	21, 125	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
127		eqid 2737	. . . . . . . . 9 ⊢ ((1...𝑁) matRRep 𝑅) = ((1...𝑁) matRRep 𝑅)
128	4, 5, 127, 49	marrepval 22527	. . . . . . . 8 ⊢ (((𝑊 ∈ 𝐵 ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ (𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))))
129	124, 126, 91, 91, 128	syl22anc 839	. . . . . . 7 ⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗))))
130	112	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))))
131	116, 129, 130	3eqtr4d 2782	. . . . . 6 ⊢ (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁) = 𝑊)
132	131	fveq2d 6845	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐷‘𝑊))
133		eqid 2737	. . . . . . . . . . . 12 ⊢ ((1...𝑁) subMat 𝑅) = ((1...𝑁) subMat 𝑅)
134	4, 133, 5	submaval 22546	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
135	124, 91, 91, 134	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
136		fzdif2 32863	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
137	89, 136	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
138		mpoeq12 7440	. . . . . . . . . . 11 ⊢ ((((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)) ∧ ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
139	137, 137, 138	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
140	135, 139	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
141		difssd 4078	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁))
142	137, 141	eqsstrrd 3958	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
143	4, 5	submabas 22543	. . . . . . . . . 10 ⊢ ((𝑊 ∈ 𝐵 ∧ (1...(𝑁 − 1)) ⊆ (1...𝑁)) → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
144	124, 142, 143	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
145	140, 144	eqeltrd 2837	. . . . . . . 8 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
146		madjusmdet.e	. . . . . . . . 9 ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)
147		eqid 2737	. . . . . . . . 9 ⊢ ((1...(𝑁 − 1)) Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅)
148		eqid 2737	. . . . . . . . 9 ⊢ (Base‘((1...(𝑁 − 1)) Mat 𝑅)) = (Base‘((1...(𝑁 − 1)) Mat 𝑅))
149	146, 147, 148, 117	mdetcl 22561	. . . . . . . 8 ⊢ ((𝑅 ∈ CRing ∧ (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅))
150	18, 145, 149	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅))
151	117, 16, 48	ringlidm 20250	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
152	21, 150, 151	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
153	4	fveq2i 6844	. . . . . . . . . . 11 ⊢ (Base‘𝐴) = (Base‘((1...𝑁) Mat 𝑅))
154	5, 153	eqtri 2760	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘((1...𝑁) Mat 𝑅))
155	124, 154	eleqtrdi 2847	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅)))
156		smadiadetr 22640	. . . . . . . . 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 839	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
158	6	fveq1i 6842	. . . . . . . . 9 ⊢ (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁))
159	16	oveqi 7380	. . . . . . . . 9 ⊢ ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
160	158, 159	eqeq12i 2755	. . . . . . . 8 ⊢ ((𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) ↔ (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅)(.r‘𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
161	157, 160	sylibr 234	. . . . . . 7 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
162	137	oveq1d 7382	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = ((1...(𝑁 − 1)) maDet 𝑅))
163	162, 146	eqtr4di 2790	. . . . . . . . 9 ⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = 𝐸)
164	163	fveq1d 6843	. . . . . . . 8 ⊢ (𝜑 → ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
165	164	oveq2d 7383	. . . . . . 7 ⊢ (𝜑 → ((1r‘𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
166	161, 165	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = ((1r‘𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
167	4, 5	submat1n 33949	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
168	87, 124, 167	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
169	168	fveq2d 6845	. . . . . 6 ⊢ (𝜑 → (𝐸‘(𝑁(subMat1‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
170	152, 166, 169	3eqtr4d 2782	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
171	132, 170	eqtr3d 2774	. . . 4 ⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
172	4, 5, 87, 3, 2, 21, 1, 10	submatminr1 33954	. . . . . 6 ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝑈)𝐽))
173		madjusmdetlem1.3	. . . . . 6 ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
174	172, 173	eqtrd 2772	. . . . 5 ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
175	174	fveq2d 6845	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐼(subMat1‘𝑀)𝐽)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
176	171, 175	eqtr4d 2775	. . 3 ⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))
177	176	oveq2d 7383	. 2 ⊢ (𝜑 → ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
178	12, 27, 177	3eqtrd 2776	1 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ∖ cdif 3887   ⊆ wss 3890  ifcif 4467  {csn 4568  ^◡ccnv 5630  –1-1-onto→wf1o 6498  ‘cfv 6499  (class class class)co 7367   ∈ cmpo 7369  1c1 11039   · cmul 11043   − cmin 11377  ℕcn 12174  ℤ_≥cuz 12788  ...cfz 13461  Basecbs 17179  ._rcmulr 17221  0_gc0g 17402  SymGrpcsymg 19344  pmSgncpsgn 19464  1_rcur 20162  Ringcrg 20214  CRingccrg 20215  ℤRHomczrh 21479   Mat cmat 22372   matRRep cmarrep 22521   subMat csubma 22541   maDet cmdat 22549   maAdju cmadu 22597   minMatR1 cminmar1 22598  subMat1csmat 33937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-addf 11117  ax-mulf 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1514  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-ot 4577  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6266  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-tpos 8176  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-sup 9355  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-xnn0 12511  df-z 12525  df-dec 12645  df-uz 12789  df-rp 12943  df-fz 13462  df-fzo 13609  df-seq 13964  df-exp 14024  df-hash 14293  df-word 14476  df-lsw 14525  df-concat 14533  df-s1 14559  df-substr 14604  df-pfx 14634  df-splice 14712  df-reverse 14721  df-s2 14810  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mhm 18751  df-submnd 18752  df-efmnd 18837  df-grp 18912  df-minusg 18913  df-mulg 19044  df-subg 19099  df-ghm 19188  df-gim 19234  df-cntz 19292  df-oppg 19321  df-symg 19345  df-pmtr 19417  df-psgn 19466  df-cmn 19757  df-abl 19758  df-mgp 20122  df-rng 20134  df-ur 20163  df-ring 20216  df-cring 20217  df-oppr 20317  df-dvdsr 20337  df-unit 20338  df-invr 20368  df-dvr 20381  df-rhm 20452  df-subrng 20523  df-subrg 20547  df-drng 20708  df-sra 21168  df-rgmod 21169  df-cnfld 21353  df-zring 21427  df-zrh 21483  df-dsmm 21712  df-frlm 21727  df-mat 22373  df-marrep 22523  df-subma 22542  df-mdet 22550  df-madu 22599  df-minmar1 22600  df-smat 33938

This theorem is referenced by:  madjusmdetlem4  33974