Theorem madjusmdetlem1 33965

Description: Lemma for madjusmdet 33969. (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 22600	. . . 4 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐽 ∈ (1...𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
9	1, 2, 3, 8	syl3anc 1374	. . 3 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
10		madjusmdetlem1.u	. . . 4 ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
11	10	fveq2i 6838	. . 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 13900	. . 3 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
20		crngring 20184	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
21	18, 20	syl 17	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
22	4, 5	minmar1cl 22599	. . . . 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 33963	. 2 ⊢ (𝜑 → (𝐷‘𝑈) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝑊)))
28		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑖 = 𝑁)
29	28	fveq2d 6839	. . . . . . . . . . . . 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 6839	. . . . . . . . . . . . 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 7378	. . . . . . . . . . 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 22597	. . . . . . . . . . . 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 4487	. . . . . . . . . . . . 13 ⊢ if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀𝐽)) = if(𝐽 = 𝐽, (1r‘𝑅), (0g‘𝑅))
54		eqid 2737	. . . . . . . . . . . . . 14 ⊢ 𝐽 = 𝐽
55	54	iftruei 4487	. . . . . . . . . . . . 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 6839	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = (𝑃‘𝑁))
61	31	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑁) = 𝐼)
62	60, 61	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃‘𝑖) = 𝐼)
63	62	oveq1d 7375	. . . . . . . . . . 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 19313	. . . . . . . . . . . . . 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 22597	. . . . . . . . . . . 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 4488	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)), (𝐼𝑀(𝑄‘𝑗))) = if((𝑄‘𝑗) = 𝐽, (1r‘𝑅), (0g‘𝑅)))
77		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (𝑄‘𝑗) = 𝐽)
78	77	fveq2d 6839	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = (◡𝑄‘𝐽))
79	69, 13	symgbasf1o 19308	. . . . . . . . . . . . . . . . . . . 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 7224	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗)
84	81, 82, 83	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄‘𝑗) = 𝐽) → (◡𝑄‘(𝑄‘𝑗)) = 𝑗)
85	36	fveq2d 6839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (◡𝑄‘(𝑄‘𝑁)) = (◡𝑄‘𝐽))
86	26, 79	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
87		madjusmdet.n	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑁 ∈ ℕ)
88		nnuz 12794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ = (ℤ≥‘1)
89	87, 88	eleqtrdi 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
90		eluzfz2 13452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92		f1ocnvfv1 7224	. . . . . . . . . . . . . . . . . . . . 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 4491	. . . . . . . . . . . 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 4517	. . . . . . . . 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 7395	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V)
109	10	oveqi 7373	. . . . . . . . . . . . . 14 ⊢ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗))
110	109	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
111	110	mpoeq3ia 7438	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
112	17, 111	eqtri 2760	. . . . . . . . . . 11 ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
113	112	ovmpt4g 7507	. . . . . . . . . 10 ⊢ ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)) ∈ V) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
114	106, 107, 108, 113	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → (𝑖𝑊𝑗) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
115	104, 114	ifeqda 4517	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑊𝑗)) = ((𝑃‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄‘𝑗)))
116	115	mpoeq3dva 7437	. . . . . . 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 19313	. . . . . . . . . . . 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 22374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃‘𝑖)𝑈(𝑄‘𝑗)) ∈ (Base‘𝑅))
123	4, 117, 5, 19, 18, 122	matbas2d 22371	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) ∈ 𝐵)
124	17, 123	eqeltrid 2841	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ 𝐵)
125	117, 48	ringidcl 20204	. . . . . . . . 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 22510	. . . . . . . 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 6839	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (𝐷‘𝑊))
133		eqid 2737	. . . . . . . . . . . 12 ⊢ ((1...𝑁) subMat 𝑅) = ((1...𝑁) subMat 𝑅)
134	4, 133, 5	submaval 22529	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
135	124, 91, 91, 134	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
136		fzdif2 32851	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
137	89, 136	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
138		mpoeq12 7433	. . . . . . . . . . 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 4090	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁))
142	137, 141	eqsstrrd 3970	. . . . . . . . . 10 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
143	4, 5	submabas 22526	. . . . . . . . . 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 22544	. . . . . . . 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 20208	. . . . . . 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 6838	. . . . . . . . . . 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 22623	. . . . . . . . 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 6836	. . . . . . . . 9 ⊢ (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁)) = (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r‘𝑅))𝑁))
159	16	oveqi 7373	. . . . . . . . 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 7375	. . . . . . . . . 10 ⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = ((1...(𝑁 − 1)) maDet 𝑅))
163	162, 146	eqtr4di 2790	. . . . . . . . 9 ⊢ (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = 𝐸)
164	163	fveq1d 6837	. . . . . . . 8 ⊢ (𝜑 → ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
165	164	oveq2d 7376	. . . . . . 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 33943	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
168	87, 124, 167	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
169	168	fveq2d 6839	. . . . . 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 33948	. . . . . 6 ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝑈)𝐽))
173		madjusmdetlem1.3	. . . . . 6 ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
174	172, 173	eqtrd 2772	. . . . 5 ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
175	174	fveq2d 6839	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐼(subMat1‘𝑀)𝐽)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
176	171, 175	eqtr4d 2775	. . 3 ⊢ (𝜑 → (𝐷‘𝑊) = (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))
177	176	oveq2d 7376	. 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 3441   ∖ cdif 3899   ⊆ wss 3902  ifcif 4480  {csn 4581  ^◡ccnv 5624  –1-1-onto→wf1o 6492  ‘cfv 6493  (class class class)co 7360   ∈ cmpo 7362  1c1 11031   · cmul 11035   − cmin 11368  ℕcn 12149  ℤ_≥cuz 12755  ...cfz 13427  Basecbs 17140  ._rcmulr 17182  0_gc0g 17363  SymGrpcsymg 19302  pmSgncpsgn 19422  1_rcur 20120  Ringcrg 20172  CRingccrg 20173  ℤRHomczrh 21458   Mat cmat 22355   matRRep cmarrep 22504   subMat csubma 22524   maDet cmdat 22532   maAdju cmadu 22580   minMatR1 cminmar1 22581  subMat1csmat 33931

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 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107  ax-addf 11109  ax-mulf 11110

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 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-ot 4590  df-uni 4865  df-int 4904  df-iun 4949  df-iin 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8105  df-tpos 8170  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-sup 9349  df-oi 9419  df-card 9855  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12150  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-6 12216  df-7 12217  df-8 12218  df-9 12219  df-n0 12406  df-xnn0 12479  df-z 12493  df-dec 12612  df-uz 12756  df-rp 12910  df-fz 13428  df-fzo 13575  df-seq 13929  df-exp 13989  df-hash 14258  df-word 14441  df-lsw 14490  df-concat 14498  df-s1 14524  df-substr 14569  df-pfx 14599  df-splice 14677  df-reverse 14686  df-s2 14775  df-struct 17078  df-sets 17095  df-slot 17113  df-ndx 17125  df-base 17141  df-ress 17162  df-plusg 17194  df-mulr 17195  df-starv 17196  df-sca 17197  df-vsca 17198  df-ip 17199  df-tset 17200  df-ple 17201  df-ds 17203  df-unif 17204  df-hom 17205  df-cco 17206  df-0g 17365  df-gsum 17366  df-prds 17371  df-pws 17373  df-mre 17509  df-mrc 17510  df-acs 17512  df-mgm 18569  df-sgrp 18648  df-mnd 18664  df-mhm 18712  df-submnd 18713  df-efmnd 18798  df-grp 18870  df-minusg 18871  df-mulg 19002  df-subg 19057  df-ghm 19146  df-gim 19192  df-cntz 19250  df-oppg 19279  df-symg 19303  df-pmtr 19375  df-psgn 19424  df-cmn 19715  df-abl 19716  df-mgp 20080  df-rng 20092  df-ur 20121  df-ring 20174  df-cring 20175  df-oppr 20277  df-dvdsr 20297  df-unit 20298  df-invr 20328  df-dvr 20341  df-rhm 20412  df-subrng 20483  df-subrg 20507  df-drng 20668  df-sra 21129  df-rgmod 21130  df-cnfld 21314  df-zring 21406  df-zrh 21462  df-dsmm 21691  df-frlm 21706  df-mat 22356  df-marrep 22506  df-subma 22525  df-mdet 22533  df-madu 22582  df-minmar1 22583  df-smat 33932

This theorem is referenced by:  madjusmdetlem4  33968