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 34229

Description: Lemma for madjusmdet 34230. (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 2762	. . 3 ⊢ (Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁)))
14		eqid 2762	. . 3 ⊢ (pmSgn‘(1...𝑁)) = (pmSgn‘(1...𝑁))
15		eqid 2762	. . 3 ⊢ (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
16		fveq2 6881	. . . . 5 ⊢ (𝑘 = 𝑖 → ((𝑃 ∘ ^◡𝑆)‘𝑘) = ((𝑃 ∘ ^◡𝑆)‘𝑖))
17	16	oveq1d 7427	. . . 4 ⊢ (𝑘 = 𝑖 → (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)))
18		fveq2 6881	. . . . 5 ⊢ (𝑙 = 𝑗 → ((𝑄 ∘ ^◡𝑇)‘𝑙) = ((𝑄 ∘ ^◡𝑇)‘𝑗))
19	18	oveq2d 7428	. . . 4 ⊢ (𝑙 = 𝑗 → (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
20	17, 19	cbvmpov 7507	. . 3 ⊢ (𝑘 ∈ (1...𝑁), 𝑙 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
21		eqid 2762	. . . . . 6 ⊢ (1...𝑁) = (1...𝑁)
22		madjusmdetlem2.p	. . . . . 6 ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))
23		eqid 2762	. . . . . 6 ⊢ (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
24	21, 22, 23, 13	fzto1st 33432	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
25	10, 24	syl 18	. . . 4 ⊢ (𝜑 → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
26		nnuz 12907	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
27	8, 26	eleqtrdi 2872	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
28		eluzfz2 13566	. . . . . . . 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 33432	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
32	29, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
33		eqid 2762	. . . . . . 7 ⊢ (inv_g‘(SymGrp‘(1...𝑁))) = (inv_g‘(SymGrp‘(1...𝑁)))
34	23, 13, 33	symginv 19478	. . . . . 6 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
35	32, 34	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
36		fzfid 14016	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
37	23	symggrp 19476	. . . . . . 7 ⊢ ((1...𝑁) ∈ Fin → (SymGrp‘(1...𝑁)) ∈ Grp)
38	36, 37	syl 18	. . . . . 6 ⊢ (𝜑 → (SymGrp‘(1...𝑁)) ∈ Grp)
39	13, 33	grpinvcl 19060	. . . . . 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 2863	. . . 4 ⊢ (𝜑 → ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
42		eqid 2762	. . . . . 6 ⊢ (+_g‘(SymGrp‘(1...𝑁))) = (+_g‘(SymGrp‘(1...𝑁)))
43	23, 13, 42	symgov 19460	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) = (𝑃 ∘ ^◡𝑆))
44	23, 13, 42	symgcl 19461	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
45	43, 44	eqeltrrd 2863	. . . 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 33432	. . . . 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 33432	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
52	29, 51	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
53	23, 13, 33	symginv 19478	. . . . . 6 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
54	52, 53	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
55	13, 33	grpinvcl 19060	. . . . . 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 2863	. . . 4 ⊢ (𝜑 → ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
58	23, 13, 42	symgov 19460	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) = (𝑄 ∘ ^◡𝑇))
59	23, 13, 42	symgcl 19461	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
60	58, 59	eqeltrrd 2863	. . . 4 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
61	49, 57, 60	syl2anc 595	. . 3 ⊢ (𝜑 → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
62	23, 13	symgbasf1o 19451	. . . . . . 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 2865	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ dom ^◡𝑆)
72		fvco 6979	. . . . 5 ⊢ ((Fun ^◡𝑆 ∧ 𝑁 ∈ dom ^◡𝑆) → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
73	67, 71, 72	syl2anc 595	. . . 4 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
74	21, 30, 23, 13	fzto1stinvn 33433	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑆‘𝑁) = 1)
75	29, 74	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑆‘𝑁) = 1)
76	75	fveq2d 6885	. . . 4 ⊢ (𝜑 → (𝑃‘(^◡𝑆‘𝑁)) = (𝑃‘1))
77	21, 22	fzto1stfv1 33430	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → (𝑃‘1) = 𝐼)
78	10, 77	syl 18	. . . 4 ⊢ (𝜑 → (𝑃‘1) = 𝐼)
79	73, 76, 78	3eqtrd 2801	. . 3 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = 𝐼)
80	23, 13	symgbasf1o 19451	. . . . . . 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 2865	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ dom ^◡𝑇)
90		fvco 6979	. . . . 5 ⊢ ((Fun ^◡𝑇 ∧ 𝑁 ∈ dom ^◡𝑇) → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
91	85, 89, 90	syl2anc 595	. . . 4 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
92	21, 50, 23, 13	fzto1stinvn 33433	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑇‘𝑁) = 1)
93	29, 92	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑇‘𝑁) = 1)
94	93	fveq2d 6885	. . . 4 ⊢ (𝜑 → (𝑄‘(^◡𝑇‘𝑁)) = (𝑄‘1))
95	21, 47	fzto1stfv1 33430	. . . . 5 ⊢ (𝐽 ∈ (1...𝑁) → (𝑄‘1) = 𝐽)
96	11, 95	syl 18	. . . 4 ⊢ (𝜑 → (𝑄‘1) = 𝐽)
97	91, 94, 96	3eqtrd 2801	. . 3 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = 𝐽)
98		crngring 20333	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
99	9, 98	syl 18	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
100	2, 1	minmar1cl 22819	. . . . 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 34228	. . 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 34226	. 2 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
104	23, 14, 13	psgnco 21744	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)))
105	36, 25, 41, 104	syl3anc 1397	. . . . . . 7 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)))
106	21, 22, 23, 13, 14	psgnfzto1st 33434	. . . . . . . . 9 ⊢ (𝐼 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
107	10, 106	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
108	23, 14, 13	psgninv 21743	. . . . . . . . . 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 33434	. . . . . . . . . 10 ⊢ (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
111	29, 110	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑆) = (-1↑(𝑁 + 1)))
112	109, 111	eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑆) = (-1↑(𝑁 + 1)))
113	107, 112	oveq12d 7430	. . . . . . 7 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)) = ((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))))
114	105, 113	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = ((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))))
115	23, 14, 13	psgnco 21744	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)))
116	36, 49, 57, 115	syl3anc 1397	. . . . . . 7 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)))
117	21, 47, 23, 13, 14	psgnfzto1st 33434	. . . . . . . . 9 ⊢ (𝐽 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
118	11, 117	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
119	23, 14, 13	psgninv 21743	. . . . . . . . . 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 33434	. . . . . . . . . 10 ⊢ (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
122	29, 121	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑇) = (-1↑(𝑁 + 1)))
123	120, 122	eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑇) = (-1↑(𝑁 + 1)))
124	118, 123	oveq12d 7430	. . . . . . 7 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)) = ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1))))
125	116, 124	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1))))
126	114, 125	oveq12d 7430	. . . . 5 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))))
127		1cnd 11208	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
128	127	negcld 11562	. . . . . . . 8 ⊢ (𝜑 → -1 ∈ ℂ)
129		fz1ssnn 13590	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℕ
130	129, 10	sselid 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℕ)
131	130	nnnn0d 12571	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ₀)
132		1nn0 12526	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ₀)
134	131, 133	nn0addcld 12575	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 1) ∈ ℕ₀)
135	128, 134	expcld 14189	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝐼 + 1)) ∈ ℂ)
136	8	nnnn0d 12571	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
137	136, 133	nn0addcld 12575	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
138	128, 137	expcld 14189	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝑁 + 1)) ∈ ℂ)
139	129, 11	sselid 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℕ)
140	139	nnnn0d 12571	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
141	140, 133	nn0addcld 12575	. . . . . . . 8 ⊢ (𝜑 → (𝐽 + 1) ∈ ℕ₀)
142	128, 141	expcld 14189	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝐽 + 1)) ∈ ℂ)
143	135, 138, 142, 138	mul4d 11428	. . . . . 6 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))))
144	128, 141, 134	expaddd 14191	. . . . . . . 8 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))))
145	130	nncnd 12255	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ ℂ)
146	139	nncnd 12255	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℂ)
147	145, 127, 146, 127	add4d 11445	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + (1 + 1)))
148		1p1e2 12370	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
149	148	oveq2i 7423	. . . . . . . . . . 11 ⊢ ((𝐼 + 𝐽) + (1 + 1)) = ((𝐼 + 𝐽) + 2)
150	147, 149	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + 2))
151	150	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑((𝐼 + 𝐽) + 2)))
152		2nn0 12527	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ₀
153	152	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ₀)
154	131, 140	nn0addcld 12575	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 + 𝐽) ∈ ℕ₀)
155	128, 153, 154	expaddd 14191	. . . . . . . . . 10 ⊢ (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · (-1↑2)))
156		neg1sqe1 14239	. . . . . . . . . . 11 ⊢ (-1↑2) = 1
157	156	oveq2i 7423	. . . . . . . . . 10 ⊢ ((-1↑(𝐼 + 𝐽)) · (-1↑2)) = ((-1↑(𝐼 + 𝐽)) · 1)
158	155, 157	eqtrdi 2813	. . . . . . . . 9 ⊢ (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · 1))
159	128, 154	expcld 14189	. . . . . . . . . 10 ⊢ (𝜑 → (-1↑(𝐼 + 𝐽)) ∈ ℂ)
160	159	mulridd 11232	. . . . . . . . 9 ⊢ (𝜑 → ((-1↑(𝐼 + 𝐽)) · 1) = (-1↑(𝐼 + 𝐽)))
161	151, 158, 160	3eqtrd 2801	. . . . . . . 8 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑(𝐼 + 𝐽)))
162	144, 161	eqtr3d 2799	. . . . . . 7 ⊢ (𝜑 → ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) = (-1↑(𝐼 + 𝐽)))
163	137	nn0zd 12622	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
164		m1expcl2 14128	. . . . . . . 8 ⊢ ((𝑁 + 1) ∈ ℤ → (-1↑(𝑁 + 1)) ∈ {-1, 1})
165		1neg1t1neg1 33094	. . . . . . . 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 7430	. . . . . 6 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))) = ((-1↑(𝐼 + 𝐽)) · 1))
168	143, 167, 160	3eqtrd 2801	. . . . 5 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (-1↑(𝐼 + 𝐽)))
169	126, 168	eqtrd 2797	. . . 4 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = (-1↑(𝐼 + 𝐽)))
170	169	fveq2d 6885	. . 3 ⊢ (𝜑 → (𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) = (𝑍‘(-1↑(𝐼 + 𝐽))))
171	170	oveq1d 7427	. 2 ⊢ (𝜑 → ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
172	103, 171	eqtrd 2797	1 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 = wceq 1569 ∈ wcel 2142 ifcif 4486 {cpr 4590 class class class wbr 5108 ↦ cmpt 5191 ^◡ccnv 5659 dom cdm 5660 ∘ ccom 5664 Fun wfun 6530 ⟶wf 6532 –1-1→wf1 6533 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7412 ∈ cmpo 7414 Fincfn 8941 1c1 11107 + caddc 11109 · cmul 11111 ≤ cle 11250 − cmin 11447 -cneg 11448 ℕcn 12239 2c2 12301 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12868 ...cfz 13541 ↑cexp 14104 Basecbs 17275 +_gcplusg 17316 ._rcmulr 17317 Grpcgrp 19006 inv_gcminusg 19007 SymGrpcsymg 19445 pmSgncpsgn 19565 Ringcrg 20321 CRingccrg 20322 ℤRHomczrh 21660 Mat cmat 22575 maDet cmdat 22752 maAdju cmadu 22800 minMatR1 cminmar1 22801 subMat1csmat 34192

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-addf 11185 ax-mulf 11186

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-xor 1541 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 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 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 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 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-tpos 8220 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-er 8692 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-sup 9400 df-oi 9470 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-xnn0 12584 df-z 12598 df-dec 12718 df-uz 12869 df-rp 13023 df-fz 13542 df-fzo 13690 df-seq 14045 df-exp 14105 df-hash 14374 df-word 14558 df-lsw 14607 df-concat 14615 df-s1 14641 df-substr 14686 df-pfx 14716 df-splice 14794 df-reverse 14803 df-s2 14892 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-hom 17340 df-cco 17341 df-0g 17500 df-gsum 17501 df-prds 17506 df-pws 17508 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-mhm 18847 df-submnd 18848 df-efmnd 18934 df-grp 19009 df-minusg 19010 df-mulg 19140 df-subg 19195 df-ghm 19290 df-gim 19335 df-cntz 19393 df-oppg 19422 df-symg 19446 df-pmtr 19518 df-psgn 19567 df-cmn 19858 df-abl 19859 df-mgp 20223 df-rng 20237 df-ur 20270 df-ring 20323 df-cring 20324 df-oppr 20426 df-dvdsr 20446 df-unit 20447 df-invr 20477 df-dvr 20490 df-rhm 20561 df-subrng 20656 df-subrg 20680 df-drng 20840 df-sra 21305 df-rgmod 21306 df-cnfld 21534 df-zring 21608 df-zrh 21664 df-dsmm 21893 df-frlm 21908 df-mat 22576 df-marrep 22726 df-subma 22745 df-mdet 22753 df-madu 22802 df-minmar1 22803 df-smat 34193

This theorem is used by: madjusmdet 34230

W3C validator