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 34462

Description: Lemma for madjusmdet 34463. (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 2760	. . 3 ⊢ (Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁)))
14		eqid 2760	. . 3 ⊢ (pmSgn‘(1...𝑁)) = (pmSgn‘(1...𝑁))
15		eqid 2760	. . 3 ⊢ (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
16		fveq2 6885	. . . . 5 ⊢ (𝑘 = 𝑖 → ((𝑃 ∘ ^◡𝑆)‘𝑘) = ((𝑃 ∘ ^◡𝑆)‘𝑖))
17	16	oveq1d 7435	. . . 4 ⊢ (𝑘 = 𝑖 → (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)))
18		fveq2 6885	. . . . 5 ⊢ (𝑙 = 𝑗 → ((𝑄 ∘ ^◡𝑇)‘𝑙) = ((𝑄 ∘ ^◡𝑇)‘𝑗))
19	18	oveq2d 7436	. . . 4 ⊢ (𝑙 = 𝑗 → (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
20	17, 19	cbvmpov 7515	. . 3 ⊢ (𝑘 ∈ (1...𝑁), 𝑙 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
21		eqid 2760	. . . . . 6 ⊢ (1...𝑁) = (1...𝑁)
22		madjusmdetlem2.p	. . . . . 6 ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))
23		eqid 2760	. . . . . 6 ⊢ (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
24	21, 22, 23, 13	fzto1st 33664	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
25	10, 24	syl 18	. . . 4 ⊢ (𝜑 → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
26		nnuz 13004	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
27	8, 26	eleqtrdi 2870	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
28		eluzfz2 13665	. . . . . . . 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 33664	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
32	29, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
33		eqid 2760	. . . . . . 7 ⊢ (inv_g‘(SymGrp‘(1...𝑁))) = (inv_g‘(SymGrp‘(1...𝑁)))
34	23, 13, 33	symginv 19616	. . . . . 6 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
35	32, 34	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
36		fzfid 14116	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
37	23	symggrp 19614	. . . . . . 7 ⊢ ((1...𝑁) ∈ Fin → (SymGrp‘(1...𝑁)) ∈ Grp)
38	36, 37	syl 18	. . . . . 6 ⊢ (𝜑 → (SymGrp‘(1...𝑁)) ∈ Grp)
39	13, 33	grpinvcl 19198	. . . . . 6 ⊢ (((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
40	38, 32, 39	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
41	35, 40	eqeltrrd 2861	. . . 4 ⊢ (𝜑 → ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
42		eqid 2760	. . . . . 6 ⊢ (+_g‘(SymGrp‘(1...𝑁))) = (+_g‘(SymGrp‘(1...𝑁)))
43	23, 13, 42	symgov 19598	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) = (𝑃 ∘ ^◡𝑆))
44	23, 13, 42	symgcl 19599	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
45	43, 44	eqeltrrd 2861	. . . 4 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃 ∘ ^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
46	25, 41, 45	syl2anc 596	. . 3 ⊢ (𝜑 → (𝑃 ∘ ^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
47		madjusmdetlem4.q	. . . . . 6 ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗)))
48	21, 47, 23, 13	fzto1st 33664	. . . . 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 33664	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
52	29, 51	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
53	23, 13, 33	symginv 19616	. . . . . 6 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
54	52, 53	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
55	13, 33	grpinvcl 19198	. . . . . 6 ⊢ (((SymGrp‘(1...𝑁)) ∈ Grp ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
56	38, 52, 55	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
57	54, 56	eqeltrrd 2861	. . . 4 ⊢ (𝜑 → ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
58	23, 13, 42	symgov 19598	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) = (𝑄 ∘ ^◡𝑇))
59	23, 13, 42	symgcl 19599	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
60	58, 59	eqeltrrd 2861	. . . 4 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
61	49, 57, 60	syl2anc 596	. . 3 ⊢ (𝜑 → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
62	23, 13	symgbasf1o 19589	. . . . . . 7 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
63	32, 62	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
64		f1of1 6823	. . . . . 6 ⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑆:(1...𝑁)–1-1→(1...𝑁))
65		df-f1 6543	. . . . . . 7 ⊢ (𝑆:(1...𝑁)–1-1→(1...𝑁) ↔ (𝑆:(1...𝑁)⟶(1...𝑁) ∧ Fun ^◡𝑆))
66	65	simprbi 503	. . . . . 6 ⊢ (𝑆:(1...𝑁)–1-1→(1...𝑁) → Fun ^◡𝑆)
67	63, 64, 66	3syl 19	. . . . 5 ⊢ (𝜑 → Fun ^◡𝑆)
68		f1ocnv 6837	. . . . . . 7 ⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → ^◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
69		f1odm 6828	. . . . . . 7 ⊢ (^◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → dom ^◡𝑆 = (1...𝑁))
70	63, 68, 69	3syl 19	. . . . . 6 ⊢ (𝜑 → dom ^◡𝑆 = (1...𝑁))
71	29, 70	eleqtrrd 2863	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ dom ^◡𝑆)
72		fvco 6983	. . . . 5 ⊢ ((Fun ^◡𝑆 ∧ 𝑁 ∈ dom ^◡𝑆) → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
73	67, 71, 72	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
74	21, 30, 23, 13	fzto1stinvn 33665	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑆‘𝑁) = 1)
75	29, 74	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑆‘𝑁) = 1)
76	75	fveq2d 6889	. . . 4 ⊢ (𝜑 → (𝑃‘(^◡𝑆‘𝑁)) = (𝑃‘1))
77	21, 22	fzto1stfv1 33662	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → (𝑃‘1) = 𝐼)
78	10, 77	syl 18	. . . 4 ⊢ (𝜑 → (𝑃‘1) = 𝐼)
79	73, 76, 78	3eqtrd 2799	. . 3 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = 𝐼)
80	23, 13	symgbasf1o 19589	. . . . . . 7 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
81	52, 80	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
82		f1of1 6823	. . . . . 6 ⊢ (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑇:(1...𝑁)–1-1→(1...𝑁))
83		df-f1 6543	. . . . . . 7 ⊢ (𝑇:(1...𝑁)–1-1→(1...𝑁) ↔ (𝑇:(1...𝑁)⟶(1...𝑁) ∧ Fun ^◡𝑇))
84	83	simprbi 503	. . . . . 6 ⊢ (𝑇:(1...𝑁)–1-1→(1...𝑁) → Fun ^◡𝑇)
85	81, 82, 84	3syl 19	. . . . 5 ⊢ (𝜑 → Fun ^◡𝑇)
86		f1ocnv 6837	. . . . . . 7 ⊢ (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → ^◡𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
87		f1odm 6828	. . . . . . 7 ⊢ (^◡𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → dom ^◡𝑇 = (1...𝑁))
88	81, 86, 87	3syl 19	. . . . . 6 ⊢ (𝜑 → dom ^◡𝑇 = (1...𝑁))
89	29, 88	eleqtrrd 2863	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ dom ^◡𝑇)
90		fvco 6983	. . . . 5 ⊢ ((Fun ^◡𝑇 ∧ 𝑁 ∈ dom ^◡𝑇) → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
91	85, 89, 90	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
92	21, 50, 23, 13	fzto1stinvn 33665	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑇‘𝑁) = 1)
93	29, 92	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑇‘𝑁) = 1)
94	93	fveq2d 6889	. . . 4 ⊢ (𝜑 → (𝑄‘(^◡𝑇‘𝑁)) = (𝑄‘1))
95	21, 47	fzto1stfv1 33662	. . . . 5 ⊢ (𝐽 ∈ (1...𝑁) → (𝑄‘1) = 𝐽)
96	11, 95	syl 18	. . . 4 ⊢ (𝜑 → (𝑄‘1) = 𝐽)
97	91, 94, 96	3eqtrd 2799	. . 3 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = 𝐽)
98		crngring 20472	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
99	9, 98	syl 18	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
100	2, 1	minmar1cl 22966	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
101	99, 12, 10, 11, 100	syl22anc 852	. . . 4 ⊢ (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
102	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 22, 30, 47, 50, 20, 101	madjusmdetlem3 34461	. . 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 34459	. 2 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
104	23, 14, 13	psgnco 21889	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)))
105	36, 25, 41, 104	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)))
106	21, 22, 23, 13, 14	psgnfzto1st 33666	. . . . . . . . 9 ⊢ (𝐼 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑃) = ( -1↑(𝐼 + 1)))
107	10, 106	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑃) = ( -1↑(𝐼 + 1)))
108	23, 14, 13	psgninv 21888	. . . . . . . . . 10 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘^◡𝑆) = ((pmSgn‘(1...𝑁))‘𝑆))
109	36, 32, 108	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑆) = ((pmSgn‘(1...𝑁))‘𝑆))
110	21, 30, 23, 13, 14	psgnfzto1st 33666	. . . . . . . . . 10 ⊢ (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑆) = ( -1↑(𝑁 + 1)))
111	29, 110	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑆) = ( -1↑(𝑁 + 1)))
112	109, 111	eqtrd 2795	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑆) = ( -1↑(𝑁 + 1)))
113	107, 112	oveq12d 7438	. . . . . . 7 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘𝑃) · ((pmSgn‘(1...𝑁))‘^◡𝑆)) = (( -1↑(𝐼 + 1)) · ( -1↑(𝑁 + 1))))
114	105, 113	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) = (( -1↑(𝐼 + 1)) · ( -1↑(𝑁 + 1))))
115	23, 14, 13	psgnco 21889	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)))
116	36, 49, 57, 115	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)))
117	21, 47, 23, 13, 14	psgnfzto1st 33666	. . . . . . . . 9 ⊢ (𝐽 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑄) = ( -1↑(𝐽 + 1)))
118	11, 117	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑄) = ( -1↑(𝐽 + 1)))
119	23, 14, 13	psgninv 21888	. . . . . . . . . 10 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → ((pmSgn‘(1...𝑁))‘^◡𝑇) = ((pmSgn‘(1...𝑁))‘𝑇))
120	36, 52, 119	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑇) = ((pmSgn‘(1...𝑁))‘𝑇))
121	21, 50, 23, 13, 14	psgnfzto1st 33666	. . . . . . . . . 10 ⊢ (𝑁 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑇) = ( -1↑(𝑁 + 1)))
122	29, 121	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑇) = ( -1↑(𝑁 + 1)))
123	120, 122	eqtrd 2795	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘^◡𝑇) = ( -1↑(𝑁 + 1)))
124	118, 123	oveq12d 7438	. . . . . . 7 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘𝑄) · ((pmSgn‘(1...𝑁))‘^◡𝑇)) = (( -1↑(𝐽 + 1)) · ( -1↑(𝑁 + 1))))
125	116, 124	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)) = (( -1↑(𝐽 + 1)) · ( -1↑(𝑁 + 1))))
126	114, 125	oveq12d 7438	. . . . 5 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = ((( -1↑(𝐼 + 1)) · ( -1↑(𝑁 + 1))) · (( -1↑(𝐽 + 1)) · ( -1↑(𝑁 + 1)))))
127		1cnd 11302	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
128	127	negcld 11656	. . . . . . . 8 ⊢ (𝜑 → -1 ∈ ℂ)
129		fz1ssnn 13689	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℕ
130	129, 10	sselid 3906	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℕ)
131	130	nnnn0d 12667	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ₀)
132		1nn0 12622	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ₀)
134	131, 133	nn0addcld 12671	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 1) ∈ ℕ₀)
135	128, 134	expcld 14289	. . . . . . 7 ⊢ (𝜑 → ( -1↑(𝐼 + 1)) ∈ ℂ)
136	8	nnnn0d 12667	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
137	136, 133	nn0addcld 12671	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
138	128, 137	expcld 14289	. . . . . . 7 ⊢ (𝜑 → ( -1↑(𝑁 + 1)) ∈ ℂ)
139	129, 11	sselid 3906	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℕ)
140	139	nnnn0d 12667	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
141	140, 133	nn0addcld 12671	. . . . . . . 8 ⊢ (𝜑 → (𝐽 + 1) ∈ ℕ₀)
142	128, 141	expcld 14289	. . . . . . 7 ⊢ (𝜑 → ( -1↑(𝐽 + 1)) ∈ ℂ)
143	135, 138, 142, 138	mul4d 11522	. . . . . 6 ⊢ (𝜑 → ((( -1↑(𝐼 + 1)) · ( -1↑(𝑁 + 1))) · (( -1↑(𝐽 + 1)) · ( -1↑(𝑁 + 1)))) = ((( -1↑(𝐼 + 1)) · ( -1↑(𝐽 + 1))) · (( -1↑(𝑁 + 1)) · ( -1↑(𝑁 + 1)))))
144	128, 141, 134	expaddd 14291	. . . . . . . 8 ⊢ (𝜑 → ( -1↑((𝐼 + 1) + (𝐽 + 1))) = (( -1↑(𝐼 + 1)) · ( -1↑(𝐽 + 1))))
145	130	nncnd 12351	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ ℂ)
146	139	nncnd 12351	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℂ)
147	145, 127, 146, 127	add4d 11539	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + (1 + 1)))
148		1p1e2 12466	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
149	148	oveq2i 7431	. . . . . . . . . . 11 ⊢ ((𝐼 + 𝐽) + (1 + 1)) = ((𝐼 + 𝐽) + 2)
150	147, 149	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + 2))
151	150	oveq2d 7436	. . . . . . . . 9 ⊢ (𝜑 → ( -1↑((𝐼 + 1) + (𝐽 + 1))) = ( -1↑((𝐼 + 𝐽) + 2)))
152		2nn0 12623	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ₀
153	152	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ₀)
154	131, 140	nn0addcld 12671	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 + 𝐽) ∈ ℕ₀)
155	128, 153, 154	expaddd 14291	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑((𝐼 + 𝐽) + 2)) = (( -1↑(𝐼 + 𝐽)) · ( -1↑2)))
156		neg1sqe1 14339	. . . . . . . . . . 11 ⊢ ( -1↑2) = 1
157	156	oveq2i 7431	. . . . . . . . . 10 ⊢ (( -1↑(𝐼 + 𝐽)) · ( -1↑2)) = (( -1↑(𝐼 + 𝐽)) · 1)
158	155, 157	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝜑 → ( -1↑((𝐼 + 𝐽) + 2)) = (( -1↑(𝐼 + 𝐽)) · 1))
159	128, 154	expcld 14289	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(𝐼 + 𝐽)) ∈ ℂ)
160	159	mulridd 11326	. . . . . . . . 9 ⊢ (𝜑 → (( -1↑(𝐼 + 𝐽)) · 1) = ( -1↑(𝐼 + 𝐽)))
161	151, 158, 160	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → ( -1↑((𝐼 + 1) + (𝐽 + 1))) = ( -1↑(𝐼 + 𝐽)))
162	144, 161	eqtr3d 2797	. . . . . . 7 ⊢ (𝜑 → (( -1↑(𝐼 + 1)) · ( -1↑(𝐽 + 1))) = ( -1↑(𝐼 + 𝐽)))
163	137	nn0zd 12718	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
164		m1expcl2 14228	. . . . . . . 8 ⊢ ((𝑁 + 1) ∈ ℤ → ( -1↑(𝑁 + 1)) ∈ { -1, 1})
165		1neg1t1neg1 33330	. . . . . . . 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 7438	. . . . . 6 ⊢ (𝜑 → ((( -1↑(𝐼 + 1)) · ( -1↑(𝐽 + 1))) · (( -1↑(𝑁 + 1)) · ( -1↑(𝑁 + 1)))) = (( -1↑(𝐼 + 𝐽)) · 1))
168	143, 167, 160	3eqtrd 2799	. . . . 5 ⊢ (𝜑 → ((( -1↑(𝐼 + 1)) · ( -1↑(𝑁 + 1))) · (( -1↑(𝐽 + 1)) · ( -1↑(𝑁 + 1)))) = ( -1↑(𝐼 + 𝐽)))
169	126, 168	eqtrd 2795	. . . 4 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = ( -1↑(𝐼 + 𝐽)))
170	169	fveq2d 6889	. . 3 ⊢ (𝜑 → (𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) = (𝑍‘( -1↑(𝐼 + 𝐽))))
171	170	oveq1d 7435	. 2 ⊢ (𝜑 → ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))) = ((𝑍‘( -1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
172	103, 171	eqtrd 2795	1 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘( -1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ifcif 4481 {cpr 4585 class class class wbr 5102 ↦ cmpt 5185 ^◡ccnv 5649 dom cdm 5650 ∘ ccom 5654 Fun wfun 6532 ⟶wf 6534 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 ∈ cmpo 7422 Fincfn 8973 1c1 11201 + caddc 11203 · cmul 11205 ≤ cle 11344 − cmin 11541 -cneg 11542 ℕcn 12335 2c2 12397 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ...cfz 13639 ↑cexp 14204 Basecbs 17387 +_gcplusg 17428 ._rcmulr 17429 Grpcgrp 19144 inv_gcminusg 19145 SymGrpcsymg 19583 pmSgncpsgn 19703 Ringcrg 20459 CRingccrg 20460 ℤRHomczrh 21805 Mat cmat 22722 maDet cmdat 22899 maAdju cmadu 22947 minMatR1 cminmar1 22948 subMat1csmat 34425

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-addf 11279 ax-mulf 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1541 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-ot 4592 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8243 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-sup 9434 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-xnn0 12680 df-z 12694 df-dec 12815 df-uz 12966 df-rp 13121 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-word 14659 df-lsw 14708 df-concat 14716 df-s1 14743 df-substr 14789 df-pfx 14821 df-splice 14899 df-reverse 14908 df-s2 14999 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-0g 17612 df-gsum 17613 df-prds 17618 df-pws 17620 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-efmnd 19065 df-grp 19147 df-minusg 19148 df-mulg 19278 df-subg 19333 df-ghm 19428 df-gim 19473 df-cntz 19531 df-oppg 19560 df-symg 19584 df-pmtr 19656 df-psgn 19705 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-cring 20462 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-dvr 20631 df-rhm 20702 df-subrng 20798 df-subrg 20822 df-drng 20982 df-sra 21448 df-rgmod 21449 df-cnfld 21679 df-zring 21753 df-zrh 21809 df-dsmm 22038 df-frlm 22053 df-mat 22723 df-marrep 22873 df-subma 22892 df-mdet 22900 df-madu 22949 df-minmar1 22950 df-smat 34426

This theorem is used by: madjusmdet 34463

W3C validator