madjusmdetlem4 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > madjusmdetlem4		Structured version Visualization version GIF version

Theorem madjusmdetlem4 34186

Description: Lemma for madjusmdet 34187. (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	⊢ (𝜑 → 𝑀 ∈ 𝐵)
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), 𝑗)))

**Assertion**
Ref	Expression
madjusmdetlem4	⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Distinct variable groups: 𝐵,𝑖,𝑗 𝑖,𝐼,𝑗 𝑖,𝐽,𝑗 𝑖,𝑀,𝑗 𝑖,𝑁,𝑗 𝑃,𝑖,𝑗 𝑄,𝑖,𝑗 𝑅,𝑖,𝑗 𝜑,𝑖,𝑗 𝑆,𝑖,𝑗 𝑇,𝑖,𝑗 Allowed substitution hints: 𝐴(𝑖,𝑗) 𝐷(𝑖,𝑗) · (𝑖,𝑗) 𝐸(𝑖,𝑗) 𝐾(𝑖,𝑗) 𝑍(𝑖,𝑗)

Proof of Theorem madjusmdetlem4 Dummy variables 𝑘 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		madjusmdet.b	. . 3 ⊢ 𝐵 = (Base‘𝐴)
2		madjusmdet.a	. . 3 ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)
3		madjusmdet.d	. . 3 ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)
4		madjusmdet.k	. . 3 ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)
5		madjusmdet.t	. . 3 ⊢ · = (._r‘𝑅)
6		madjusmdet.z	. . 3 ⊢ 𝑍 = (ℤRHom‘𝑅)
7		madjusmdet.e	. . 3 ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)
8		madjusmdet.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		madjusmdet.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ CRing)
10		madjusmdet.i	. . 3 ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))
11		madjusmdet.j	. . 3 ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))
12		madjusmdet.m	. . 3 ⊢ (𝜑 → 𝑀 ∈ 𝐵)
13		eqid 2761	. . 3 ⊢ (Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁)))
14		eqid 2761	. . 3 ⊢ (pmSgn‘(1...𝑁)) = (pmSgn‘(1...𝑁))
15		eqid 2761	. . 3 ⊢ (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
16		fveq2 6881	. . . . 5 ⊢ (𝑘 = 𝑖 → ((𝑃 ∘ ^◡𝑆)‘𝑘) = ((𝑃 ∘ ^◡𝑆)‘𝑖))
17	16	oveq1d 7425	. . . 4 ⊢ (𝑘 = 𝑖 → (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)))
18		fveq2 6881	. . . . 5 ⊢ (𝑙 = 𝑗 → ((𝑄 ∘ ^◡𝑇)‘𝑙) = ((𝑄 ∘ ^◡𝑇)‘𝑗))
19	18	oveq2d 7426	. . . 4 ⊢ (𝑙 = 𝑗 → (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
20	17, 19	cbvmpov 7505	. . 3 ⊢ (𝑘 ∈ (1...𝑁), 𝑙 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
21		eqid 2761	. . . . . 6 ⊢ (1...𝑁) = (1...𝑁)
22		madjusmdetlem2.p	. . . . . 6 ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))
23		eqid 2761	. . . . . 6 ⊢ (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
24	21, 22, 23, 13	fzto1st 33389	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
25	10, 24	syl 18	. . . 4 ⊢ (𝜑 → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
26		nnuz 12900	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
27	8, 26	eleqtrdi 2871	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
28		eluzfz2 13559	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
29	27, 28	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
30		madjusmdetlem2.s	. . . . . . . 8 ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖)))
31	21, 30, 23, 13	fzto1st 33389	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
32	29, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
33		eqid 2761	. . . . . . 7 ⊢ (inv_g‘(SymGrp‘(1...𝑁))) = (inv_g‘(SymGrp‘(1...𝑁)))
34	23, 13, 33	symginv 19471	. . . . . 6 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
35	32, 34	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
36		fzfid 14008	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
37	23	symggrp 19469	. . . . . . 7 ⊢ ((1...𝑁) ∈ Fin → (SymGrp‘(1...𝑁)) ∈ Grp)
38	36, 37	syl 18	. . . . . 6 ⊢ (𝜑 → (SymGrp‘(1...𝑁)) ∈ Grp)
39	13, 33	grpinvcl 19053	. . . . . 6 ⊢ (((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
40	38, 32, 39	syl2anc 595	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
41	35, 40	eqeltrrd 2862	. . . 4 ⊢ (𝜑 → ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
42		eqid 2761	. . . . . 6 ⊢ (+_g‘(SymGrp‘(1...𝑁))) = (+_g‘(SymGrp‘(1...𝑁)))
43	23, 13, 42	symgov 19453	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) = (𝑃 ∘ ^◡𝑆))
44	23, 13, 42	symgcl 19454	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
45	43, 44	eqeltrrd 2862	. . . 4 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃 ∘ ^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
46	25, 41, 45	syl2anc 595	. . 3 ⊢ (𝜑 → (𝑃 ∘ ^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
47		madjusmdetlem4.q	. . . . . 6 ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗)))
48	21, 47, 23, 13	fzto1st 33389	. . . . 5 ⊢ (𝐽 ∈ (1...𝑁) → 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))))
49	11, 48	syl 18	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))))
50		madjusmdetlem4.t	. . . . . . . 8 ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗)))
51	21, 50, 23, 13	fzto1st 33389	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
52	29, 51	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
53	23, 13, 33	symginv 19471	. . . . . 6 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
54	52, 53	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
55	13, 33	grpinvcl 19053	. . . . . 6 ⊢ (((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
56	38, 52, 55	syl2anc 595	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
57	54, 56	eqeltrrd 2862	. . . 4 ⊢ (𝜑 → ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
58	23, 13, 42	symgov 19453	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) = (𝑄 ∘ ^◡𝑇))
59	23, 13, 42	symgcl 19454	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
60	58, 59	eqeltrrd 2862	. . . 4 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
61	49, 57, 60	syl2anc 595	. . 3 ⊢ (𝜑 → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
62	23, 13	symgbasf1o 19444	. . . . . . 7 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
63	32, 62	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
64		f1of1 6819	. . . . . 6 ⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑆:(1...𝑁)–1-1→(1...𝑁))
65		df-f1 6541	. . . . . . 7 ⊢ (𝑆:(1...𝑁)–1-1→(1...𝑁) ↔ (𝑆:(1...𝑁)⟶(1...𝑁) ∧ Fun ^◡𝑆))
66	65	simprbi 502	. . . . . 6 ⊢ (𝑆:(1...𝑁)–1-1→(1...𝑁) → Fun ^◡𝑆)
67	63, 64, 66	3syl 19	. . . . 5 ⊢ (𝜑 → Fun ^◡𝑆)
68		f1ocnv 6833	. . . . . . 7 ⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → ^◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
69		f1odm 6824	. . . . . . 7 ⊢ (^◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → dom ^◡𝑆 = (1...𝑁))
70	63, 68, 69	3syl 19	. . . . . 6 ⊢ (𝜑 → dom ^◡𝑆 = (1...𝑁))
71	29, 70	eleqtrrd 2864	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ dom ^◡𝑆)
72		fvco 6979	. . . . 5 ⊢ ((Fun ^◡𝑆 ∧ 𝑁 ∈ dom ^◡𝑆) → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
73	67, 71, 72	syl2anc 595	. . . 4 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
74	21, 30, 23, 13	fzto1stinvn 33390	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑆‘𝑁) = 1)
75	29, 74	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑆‘𝑁) = 1)
76	75	fveq2d 6885	. . . 4 ⊢ (𝜑 → (𝑃‘(^◡𝑆‘𝑁)) = (𝑃‘1))
77	21, 22	fzto1stfv1 33387	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → (𝑃‘1) = 𝐼)
78	10, 77	syl 18	. . . 4 ⊢ (𝜑 → (𝑃‘1) = 𝐼)
79	73, 76, 78	3eqtrd 2800	. . 3 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = 𝐼)
80	23, 13	symgbasf1o 19444	. . . . . . 7 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
81	52, 80	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
82		f1of1 6819	. . . . . 6 ⊢ (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑇:(1...𝑁)–1-1→(1...𝑁))
83		df-f1 6541	. . . . . . 7 ⊢ (𝑇:(1...𝑁)–1-1→(1...𝑁) ↔ (𝑇:(1...𝑁)⟶(1...𝑁) ∧ Fun ^◡𝑇))
84	83	simprbi 502	. . . . . 6 ⊢ (𝑇:(1...𝑁)–1-1→(1...𝑁) → Fun ^◡𝑇)
85	81, 82, 84	3syl 19	. . . . 5 ⊢ (𝜑 → Fun ^◡𝑇)
86		f1ocnv 6833	. . . . . . 7 ⊢ (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → ^◡𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
87		f1odm 6824	. . . . . . 7 ⊢ (^◡𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → dom ^◡𝑇 = (1...𝑁))
88	81, 86, 87	3syl 19	. . . . . 6 ⊢ (𝜑 → dom ^◡𝑇 = (1...𝑁))
89	29, 88	eleqtrrd 2864	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ dom ^◡𝑇)
90		fvco 6979	. . . . 5 ⊢ ((Fun ^◡𝑇 ∧ 𝑁 ∈ dom ^◡𝑇) → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
91	85, 89, 90	syl2anc 595	. . . 4 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
92	21, 50, 23, 13	fzto1stinvn 33390	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑇‘𝑁) = 1)
93	29, 92	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑇‘𝑁) = 1)
94	93	fveq2d 6885	. . . 4 ⊢ (𝜑 → (𝑄‘(^◡𝑇‘𝑁)) = (𝑄‘1))
95	21, 47	fzto1stfv1 33387	. . . . 5 ⊢ (𝐽 ∈ (1...𝑁) → (𝑄‘1) = 𝐽)
96	11, 95	syl 18	. . . 4 ⊢ (𝜑 → (𝑄‘1) = 𝐽)
97	91, 94, 96	3eqtrd 2800	. . 3 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = 𝐽)
98		crngring 20326	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
99	9, 98	syl 18	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
100	2, 1	minmar1cl 22787	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
101	99, 12, 10, 11, 100	syl22anc 851	. . . 4 ⊢ (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
102	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 22, 30, 47, 50, 20, 101	madjusmdetlem3 34185	. . 3 ⊢ (𝜑 → (𝐼(subMat1‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))𝐽) = (𝑁(subMat1‘(𝑘 ∈ (1...𝑁), 𝑙 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙))))𝑁))
103	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 20, 46, 61, 79, 97, 102	madjusmdetlem1 34183	. 2 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
104	23, 14, 13	psgnco 21712	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)))
105	36, 25, 41, 104	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)))
106	21, 22, 23, 13, 14	psgnfzto1st 33391	. . . . . . . . 9 ⊢ (𝐼 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
107	10, 106	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
108	23, 14, 13	psgninv 21711	. . . . . . . . . 10 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘^◡𝑆) = ((pmSgn‘(1...𝑁))‘𝑆))
109	36, 32, 108	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑆) = ((pmSgn‘(1...𝑁))‘𝑆))
110	21, 30, 23, 13, 14	psgnfzto1st 33391	. . . . . . . . . 10 ⊢ (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
111	29, 110	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
112	109, 111	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑆) = (-1↑(𝑁 + 1)))
113	107, 112	oveq12d 7428	. . . . . . 7 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)) = ((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))))
114	105, 113	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = ((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))))
115	23, 14, 13	psgnco 21712	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)))
116	36, 49, 57, 115	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)))
117	21, 47, 23, 13, 14	psgnfzto1st 33391	. . . . . . . . 9 ⊢ (𝐽 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
118	11, 117	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
119	23, 14, 13	psgninv 21711	. . . . . . . . . 10 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘^◡𝑇) = ((pmSgn‘(1...𝑁))‘𝑇))
120	36, 52, 119	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑇) = ((pmSgn‘(1...𝑁))‘𝑇))
121	21, 50, 23, 13, 14	psgnfzto1st 33391	. . . . . . . . . 10 ⊢ (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
122	29, 121	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
123	120, 122	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑇) = (-1↑(𝑁 + 1)))
124	118, 123	oveq12d 7428	. . . . . . 7 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)) = ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1))))
125	116, 124	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1))))
126	114, 125	oveq12d 7428	. . . . 5 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))))
127		1cnd 11201	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
128	127	negcld 11555	. . . . . . . 8 ⊢ (𝜑 → -1 ∈ ℂ)
129		fz1ssnn 13582	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℕ
130	129, 10	sselid 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℕ)
131	130	nnnn0d 12564	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ₀)
132		1nn0 12519	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ₀)
134	131, 133	nn0addcld 12568	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 1) ∈ ℕ₀)
135	128, 134	expcld 14181	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝐼 + 1)) ∈ ℂ)
136	8	nnnn0d 12564	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
137	136, 133	nn0addcld 12568	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
138	128, 137	expcld 14181	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝑁 + 1)) ∈ ℂ)
139	129, 11	sselid 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℕ)
140	139	nnnn0d 12564	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
141	140, 133	nn0addcld 12568	. . . . . . . 8 ⊢ (𝜑 → (𝐽 + 1) ∈ ℕ₀)
142	128, 141	expcld 14181	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝐽 + 1)) ∈ ℂ)
143	135, 138, 142, 138	mul4d 11421	. . . . . 6 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))))
144	128, 141, 134	expaddd 14183	. . . . . . . 8 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))))
145	130	nncnd 12248	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ ℂ)
146	139	nncnd 12248	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℂ)
147	145, 127, 146, 127	add4d 11438	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + (1 + 1)))
148		1p1e2 12363	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
149	148	oveq2i 7421	. . . . . . . . . . 11 ⊢ ((𝐼 + 𝐽) + (1 + 1)) = ((𝐼 + 𝐽) + 2)
150	147, 149	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + 2))
151	150	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑((𝐼 + 𝐽) + 2)))
152		2nn0 12520	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ₀
153	152	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ₀)
154	131, 140	nn0addcld 12568	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 + 𝐽) ∈ ℕ₀)
155	128, 153, 154	expaddd 14183	. . . . . . . . . 10 ⊢ (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · (-1↑2)))
156		neg1sqe1 14231	. . . . . . . . . . 11 ⊢ (-1↑2) = 1
157	156	oveq2i 7421	. . . . . . . . . 10 ⊢ ((-1↑(𝐼 + 𝐽)) · (-1↑2)) = ((-1↑(𝐼 + 𝐽)) · 1)
158	155, 157	eqtrdi 2812	. . . . . . . . 9 ⊢ (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · 1))
159	128, 154	expcld 14181	. . . . . . . . . 10 ⊢ (𝜑 → (-1↑(𝐼 + 𝐽)) ∈ ℂ)
160	159	mulridd 11225	. . . . . . . . 9 ⊢ (𝜑 → ((-1↑(𝐼 + 𝐽)) · 1) = (-1↑(𝐼 + 𝐽)))
161	151, 158, 160	3eqtrd 2800	. . . . . . . 8 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑(𝐼 + 𝐽)))
162	144, 161	eqtr3d 2798	. . . . . . 7 ⊢ (𝜑 → ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) = (-1↑(𝐼 + 𝐽)))
163	137	nn0zd 12615	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
164		m1expcl2 14120	. . . . . . . 8 ⊢ ((𝑁 + 1) ∈ ℤ → (-1↑(𝑁 + 1)) ∈ {-1, 1})
165		1neg1t1neg1 33049	. . . . . . . 8 ⊢ ((-1↑(𝑁 + 1)) ∈ {-1, 1} → ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1))) = 1)
166	163, 164, 165	3syl 19	. . . . . . 7 ⊢ (𝜑 → ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1))) = 1)
167	162, 166	oveq12d 7428	. . . . . 6 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))) = ((-1↑(𝐼 + 𝐽)) · 1))
168	143, 167, 160	3eqtrd 2800	. . . . 5 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (-1↑(𝐼 + 𝐽)))
169	126, 168	eqtrd 2796	. . . 4 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = (-1↑(𝐼 + 𝐽)))
170	169	fveq2d 6885	. . 3 ⊢ (𝜑 → (𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) = (𝑍‘(-1↑(𝐼 + 𝐽))))
171	170	oveq1d 7425	. 2 ⊢ (𝜑 → ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
172	103, 171	eqtrd 2796	1 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1568 ∈ wcel 2141 ifcif 4486 {cpr 4590 class class class wbr 5108 ↦ cmpt 5191 ^◡ccnv 5660 dom cdm 5661 ∘ ccom 5665 Fun wfun 6530 ⟶wf 6532 –1-1→wf1 6533 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 Fincfn 8942 1c1 11100 + caddc 11102 · cmul 11104 ≤ cle 11243 − cmin 11440 -cneg 11441 ℕcn 12232 2c2 12294 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ...cfz 13534 ↑cexp 14096 Basecbs 17268 +_gcplusg 17309 ._rcmulr 17310 Grpcgrp 18999 inv_gcminusg 19000 SymGrpcsymg 19438 pmSgncpsgn 19558 Ringcrg 20314 CRingccrg 20315 ℤRHomczrh 21628 Mat cmat 22543 maDet cmdat 22720 maAdju cmadu 22768 minMatR1 cminmar1 22769 subMat1csmat 34149

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-addf 11178 ax-mulf 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-xor 1540 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-ot 4597 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-rp 13016 df-fz 13535 df-fzo 13682 df-seq 14037 df-exp 14097 df-hash 14366 df-word 14550 df-lsw 14599 df-concat 14607 df-s1 14633 df-substr 14678 df-pfx 14708 df-splice 14786 df-reverse 14795 df-s2 14884 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-0g 17493 df-gsum 17494 df-prds 17499 df-pws 17501 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-efmnd 18927 df-grp 19002 df-minusg 19003 df-mulg 19133 df-subg 19188 df-ghm 19283 df-gim 19328 df-cntz 19386 df-oppg 19415 df-symg 19439 df-pmtr 19511 df-psgn 19560 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-rhm 20553 df-subrng 20630 df-subrg 20654 df-drng 20814 df-sra 21273 df-rgmod 21274 df-cnfld 21502 df-zring 21576 df-zrh 21632 df-dsmm 21861 df-frlm 21876 df-mat 22544 df-marrep 22694 df-subma 22713 df-mdet 22721 df-madu 22770 df-minmar1 22771 df-smat 34150

This theorem is referenced by: madjusmdet 34187

W3C validator