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 34327

Description: Lemma for madjusmdet 34328. (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 6882	. . . . 5 ⊢ (𝑘 = 𝑖 → ((𝑃 ∘ ^◡𝑆)‘𝑘) = ((𝑃 ∘ ^◡𝑆)‘𝑖))
17	16	oveq1d 7431	. . . 4 ⊢ (𝑘 = 𝑖 → (((𝑃 ∘ ^◡𝑆)‘𝑘)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)))
18		fveq2 6882	. . . . 5 ⊢ (𝑙 = 𝑗 → ((𝑄 ∘ ^◡𝑇)‘𝑙) = ((𝑄 ∘ ^◡𝑇)‘𝑗))
19	18	oveq2d 7432	. . . 4 ⊢ (𝑙 = 𝑗 → (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑙)) = (((𝑃 ∘ ^◡𝑆)‘𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)((𝑄 ∘ ^◡𝑇)‘𝑗)))
20	17, 19	cbvmpov 7511	. . 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 33530	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
25	10, 24	syl 18	. . . 4 ⊢ (𝜑 → 𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))))
26		nnuz 12929	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
27	8, 26	eleqtrdi 2872	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
28		eluzfz2 13588	. . . . . . . 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 33530	. . . . . . 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 19530	. . . . . 6 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
35	32, 34	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑆) = ^◡𝑆)
36		fzfid 14039	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
37	23	symggrp 19528	. . . . . . 7 ⊢ ((1...𝑁) ∈ Fin → (SymGrp‘(1...𝑁)) ∈ Grp)
38	36, 37	syl 18	. . . . . 6 ⊢ (𝜑 → (SymGrp‘(1...𝑁)) ∈ Grp)
39	13, 33	grpinvcl 19112	. . . . . 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 2863	. . . 4 ⊢ (𝜑 → ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
42		eqid 2762	. . . . . 6 ⊢ (+_g‘(SymGrp‘(1...𝑁))) = (+_g‘(SymGrp‘(1...𝑁)))
43	23, 13, 42	symgov 19512	. . . . 5 ⊢ ((𝑃 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑃(+_g‘(SymGrp‘(1...𝑁)))^◡𝑆) = (𝑃 ∘ ^◡𝑆))
44	23, 13, 42	symgcl 19513	. . . . 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 596	. . 3 ⊢ (𝜑 → (𝑃 ∘ ^◡𝑆) ∈ (Base‘(SymGrp‘(1...𝑁))))
47		madjusmdetlem4.q	. . . . . 6 ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗)))
48	21, 47, 23, 13	fzto1st 33530	. . . . 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 33530	. . . . . . 7 ⊢ (𝑁 ∈ (1...𝑁) → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
52	29, 51	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
53	23, 13, 33	symginv 19530	. . . . . 6 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
54	52, 53	syl 18	. . . . 5 ⊢ (𝜑 → ((inv_g‘(SymGrp‘(1...𝑁)))‘𝑇) = ^◡𝑇)
55	13, 33	grpinvcl 19112	. . . . . 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 2863	. . . 4 ⊢ (𝜑 → ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))))
58	23, 13, 42	symgov 19512	. . . . 5 ⊢ ((𝑄 ∈ (Base‘(SymGrp‘(1...𝑁))) ∧ ^◡𝑇 ∈ (Base‘(SymGrp‘(1...𝑁)))) → (𝑄(+_g‘(SymGrp‘(1...𝑁)))^◡𝑇) = (𝑄 ∘ ^◡𝑇))
59	23, 13, 42	symgcl 19513	. . . . 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 596	. . 3 ⊢ (𝜑 → (𝑄 ∘ ^◡𝑇) ∈ (Base‘(SymGrp‘(1...𝑁))))
62	23, 13	symgbasf1o 19503	. . . . . . 7 ⊢ (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
63	32, 62	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
64		f1of1 6820	. . . . . 6 ⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑆:(1...𝑁)–1-1→(1...𝑁))
65		df-f1 6542	. . . . . . 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 6834	. . . . . . 7 ⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → ^◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
69		f1odm 6825	. . . . . . 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 6980	. . . . 5 ⊢ ((Fun ^◡𝑆 ∧ 𝑁 ∈ dom ^◡𝑆) → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
73	67, 71, 72	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = (𝑃‘(^◡𝑆‘𝑁)))
74	21, 30, 23, 13	fzto1stinvn 33531	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑆‘𝑁) = 1)
75	29, 74	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑆‘𝑁) = 1)
76	75	fveq2d 6886	. . . 4 ⊢ (𝜑 → (𝑃‘(^◡𝑆‘𝑁)) = (𝑃‘1))
77	21, 22	fzto1stfv1 33528	. . . . 5 ⊢ (𝐼 ∈ (1...𝑁) → (𝑃‘1) = 𝐼)
78	10, 77	syl 18	. . . 4 ⊢ (𝜑 → (𝑃‘1) = 𝐼)
79	73, 76, 78	3eqtrd 2801	. . 3 ⊢ (𝜑 → ((𝑃 ∘ ^◡𝑆)‘𝑁) = 𝐼)
80	23, 13	symgbasf1o 19503	. . . . . . 7 ⊢ (𝑇 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
81	52, 80	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
82		f1of1 6820	. . . . . 6 ⊢ (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑇:(1...𝑁)–1-1→(1...𝑁))
83		df-f1 6542	. . . . . . 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 6834	. . . . . . 7 ⊢ (𝑇:(1...𝑁)–1-1-onto→(1...𝑁) → ^◡𝑇:(1...𝑁)–1-1-onto→(1...𝑁))
87		f1odm 6825	. . . . . . 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 6980	. . . . 5 ⊢ ((Fun ^◡𝑇 ∧ 𝑁 ∈ dom ^◡𝑇) → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
91	85, 89, 90	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = (𝑄‘(^◡𝑇‘𝑁)))
92	21, 50, 23, 13	fzto1stinvn 33531	. . . . . 6 ⊢ (𝑁 ∈ (1...𝑁) → (^◡𝑇‘𝑁) = 1)
93	29, 92	syl 18	. . . . 5 ⊢ (𝜑 → (^◡𝑇‘𝑁) = 1)
94	93	fveq2d 6886	. . . 4 ⊢ (𝜑 → (𝑄‘(^◡𝑇‘𝑁)) = (𝑄‘1))
95	21, 47	fzto1stfv1 33528	. . . . 5 ⊢ (𝐽 ∈ (1...𝑁) → (𝑄‘1) = 𝐽)
96	11, 95	syl 18	. . . 4 ⊢ (𝜑 → (𝑄‘1) = 𝐽)
97	91, 94, 96	3eqtrd 2801	. . 3 ⊢ (𝜑 → ((𝑄 ∘ ^◡𝑇)‘𝑁) = 𝐽)
98		crngring 20385	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
99	9, 98	syl 18	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
100	2, 1	minmar1cl 22874	. . . . 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 34326	. . 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 34324	. 2 ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
104	23, 14, 13	psgnco 21797	. . . . . . . 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 33532	. . . . . . . . 9 ⊢ (𝐼 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
107	10, 106	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑃) = (-1↑(𝐼 + 1)))
108	23, 14, 13	psgninv 21796	. . . . . . . . . 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 33532	. . . . . . . . . 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 7434	. . . . . . 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 21797	. . . . . . . 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 33532	. . . . . . . . 9 ⊢ (𝐽 ∈ (1...𝑁) → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
118	11, 117	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((pmSgn‘(1...𝑁))‘𝑄) = (-1↑(𝐽 + 1)))
119	23, 14, 13	psgninv 21796	. . . . . . . . . 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 33532	. . . . . . . . . 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 7434	. . . . . . 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 7434	. . . . 5 ⊢ (𝜑 → (((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇))) = (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))))
127		1cnd 11229	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
128	127	negcld 11583	. . . . . . . 8 ⊢ (𝜑 → -1 ∈ ℂ)
129		fz1ssnn 13612	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℕ
130	129, 10	sselid 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℕ)
131	130	nnnn0d 12592	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ₀)
132		1nn0 12547	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℕ₀)
134	131, 133	nn0addcld 12596	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 1) ∈ ℕ₀)
135	128, 134	expcld 14212	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝐼 + 1)) ∈ ℂ)
136	8	nnnn0d 12592	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
137	136, 133	nn0addcld 12596	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
138	128, 137	expcld 14212	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝑁 + 1)) ∈ ℂ)
139	129, 11	sselid 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℕ)
140	139	nnnn0d 12592	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
141	140, 133	nn0addcld 12596	. . . . . . . 8 ⊢ (𝜑 → (𝐽 + 1) ∈ ℕ₀)
142	128, 141	expcld 14212	. . . . . . 7 ⊢ (𝜑 → (-1↑(𝐽 + 1)) ∈ ℂ)
143	135, 138, 142, 138	mul4d 11449	. . . . . 6 ⊢ (𝜑 → (((-1↑(𝐼 + 1)) · (-1↑(𝑁 + 1))) · ((-1↑(𝐽 + 1)) · (-1↑(𝑁 + 1)))) = (((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))) · ((-1↑(𝑁 + 1)) · (-1↑(𝑁 + 1)))))
144	128, 141, 134	expaddd 14214	. . . . . . . 8 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = ((-1↑(𝐼 + 1)) · (-1↑(𝐽 + 1))))
145	130	nncnd 12276	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ ℂ)
146	139	nncnd 12276	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℂ)
147	145, 127, 146, 127	add4d 11466	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + (1 + 1)))
148		1p1e2 12391	. . . . . . . . . . . 12 ⊢ (1 + 1) = 2
149	148	oveq2i 7427	. . . . . . . . . . 11 ⊢ ((𝐼 + 𝐽) + (1 + 1)) = ((𝐼 + 𝐽) + 2)
150	147, 149	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + (𝐽 + 1)) = ((𝐼 + 𝐽) + 2))
151	150	oveq2d 7432	. . . . . . . . 9 ⊢ (𝜑 → (-1↑((𝐼 + 1) + (𝐽 + 1))) = (-1↑((𝐼 + 𝐽) + 2)))
152		2nn0 12548	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ₀
153	152	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ₀)
154	131, 140	nn0addcld 12596	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 + 𝐽) ∈ ℕ₀)
155	128, 153, 154	expaddd 14214	. . . . . . . . . 10 ⊢ (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · (-1↑2)))
156		neg1sqe1 14262	. . . . . . . . . . 11 ⊢ (-1↑2) = 1
157	156	oveq2i 7427	. . . . . . . . . 10 ⊢ ((-1↑(𝐼 + 𝐽)) · (-1↑2)) = ((-1↑(𝐼 + 𝐽)) · 1)
158	155, 157	eqtrdi 2813	. . . . . . . . 9 ⊢ (𝜑 → (-1↑((𝐼 + 𝐽) + 2)) = ((-1↑(𝐼 + 𝐽)) · 1))
159	128, 154	expcld 14212	. . . . . . . . . 10 ⊢ (𝜑 → (-1↑(𝐼 + 𝐽)) ∈ ℂ)
160	159	mulridd 11253	. . . . . . . . 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 12643	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
164		m1expcl2 14151	. . . . . . . 8 ⊢ ((𝑁 + 1) ∈ ℤ → (-1↑(𝑁 + 1)) ∈ {-1, 1})
165		1neg1t1neg1 33196	. . . . . . . 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 7434	. . . . . 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 6886	. . 3 ⊢ (𝜑 → (𝑍‘(((pmSgn‘(1...𝑁))‘(𝑃 ∘ ^◡𝑆)) · ((pmSgn‘(1...𝑁))‘(𝑄 ∘ ^◡𝑇)))) = (𝑍‘(-1↑(𝐼 + 𝐽))))
171	170	oveq1d 7431	. 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 401 = wceq 1570 ∈ wcel 2145 ifcif 4485 {cpr 4589 class class class wbr 5107 ↦ cmpt 5190 ^◡ccnv 5658 dom cdm 5659 ∘ ccom 5663 Fun wfun 6531 ⟶wf 6533 –1-1→wf1 6534 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7416 ∈ cmpo 7418 Fincfn 8955 1c1 11128 + caddc 11130 · cmul 11132 ≤ cle 11271 − cmin 11468 -cneg 11469 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℤcz 12618 ℤ_≥cuz 12890 ...cfz 13563 ↑cexp 14127 Basecbs 17305 +_gcplusg 17346 ._rcmulr 17347 Grpcgrp 19058 inv_gcminusg 19059 SymGrpcsymg 19497 pmSgncpsgn 19617 Ringcrg 20373 CRingccrg 20374 ℤRHomczrh 21713 Mat cmat 22630 maDet cmdat 22807 maAdju cmadu 22855 minMatR1 cminmar1 22856 subMat1csmat 34290

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-addf 11206 ax-mulf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 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 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-ot 4596 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-tpos 8227 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-sup 9415 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-xnn0 12605 df-z 12619 df-dec 12740 df-uz 12891 df-rp 13045 df-fz 13564 df-fzo 13712 df-seq 14068 df-exp 14128 df-hash 14397 df-word 14581 df-lsw 14630 df-concat 14638 df-s1 14665 df-substr 14711 df-pfx 14743 df-splice 14821 df-reverse 14830 df-s2 14921 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-hom 17370 df-cco 17371 df-0g 17530 df-gsum 17531 df-prds 17536 df-pws 17538 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-mhm 18892 df-submnd 18893 df-efmnd 18979 df-grp 19061 df-minusg 19062 df-mulg 19192 df-subg 19247 df-ghm 19342 df-gim 19387 df-cntz 19445 df-oppg 19474 df-symg 19498 df-pmtr 19570 df-psgn 19619 df-cmn 19910 df-abl 19911 df-mgp 20275 df-rng 20289 df-ur 20322 df-ring 20375 df-cring 20376 df-oppr 20479 df-dvdsr 20499 df-unit 20500 df-invr 20530 df-dvr 20543 df-rhm 20614 df-subrng 20709 df-subrg 20733 df-drng 20893 df-sra 21358 df-rgmod 21359 df-cnfld 21587 df-zring 21661 df-zrh 21717 df-dsmm 21946 df-frlm 21961 df-mat 22631 df-marrep 22781 df-subma 22800 df-mdet 22808 df-madu 22857 df-minmar1 22858 df-smat 34291

This theorem is used by: madjusmdet 34328

W3C validator