Theorem mdetpmtr1 31345

Description: The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.)

Hypotheses

Ref	Expression
mdetpmtr.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetpmtr.b	⊢ 𝐵 = (Base‘𝐴)
mdetpmtr.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetpmtr.g	⊢ 𝐺 = (Base‘(SymGrp‘𝑁))
mdetpmtr.s	⊢ 𝑆 = (pmSgn‘𝑁)
mdetpmtr.z	⊢ 𝑍 = (ℤRHom‘𝑅)
mdetpmtr.t	⊢ · = (.r‘𝑅)
mdetpmtr1.e	⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))

Assertion

Ref	Expression
mdetpmtr1	⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)))

Distinct variable groups:   𝐵,𝑖,𝑗   𝑖,𝐺,𝑗   𝑖,𝑀,𝑗   𝑖,𝑁,𝑗   𝑃,𝑖,𝑗   𝑅,𝑖,𝑗

Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐷(𝑖,𝑗)   𝑆(𝑖,𝑗)   · (𝑖,𝑗)   𝐸(𝑖,𝑗)   𝑍(𝑖,𝑗)

Proof of Theorem mdetpmtr1

Dummy variables 𝑝 𝑞 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2738	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2738	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
3		eqid 2738	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		mdetpmtr.t	. . 3 ⊢ · = (.r‘𝑅)
5		crngring 19428	. . . 4 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
6	5	ad2antrr 726	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ Ring)
7		mdetpmtr.g	. . . . 5 ⊢ 𝐺 = (Base‘(SymGrp‘𝑁))
8	7	fvexi 6688	. . . 4 ⊢ 𝐺 ∈ V
9	8	a1i 11	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ V)
10		simplr 769	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑁 ∈ Fin)
11		mdetpmtr.s	. . . . . . 7 ⊢ 𝑆 = (pmSgn‘𝑁)
12	11, 7	psgndmfi 30942	. . . . . 6 ⊢ (𝑁 ∈ Fin → 𝑆 Fn 𝐺)
13		fnfun 6438	. . . . . 6 ⊢ (𝑆 Fn 𝐺 → Fun 𝑆)
14	10, 12, 13	3syl 18	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → Fun 𝑆)
15		simprr 773	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ 𝐺)
16		fndm 6440	. . . . . . 7 ⊢ (𝑆 Fn 𝐺 → dom 𝑆 = 𝐺)
17	10, 12, 16	3syl 18	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → dom 𝑆 = 𝐺)
18	15, 17	eleqtrrd 2836	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑃 ∈ dom 𝑆)
19		fvco 6766	. . . . 5 ⊢ ((Fun 𝑆 ∧ 𝑃 ∈ dom 𝑆) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃)))
20	14, 18, 19	syl2anc 587	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃)))
21		mdetpmtr.z	. . . . . 6 ⊢ 𝑍 = (ℤRHom‘𝑅)
22	7, 11, 21	zrhpsgnelbas 20410	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅))
23	6, 10, 15, 22	syl3anc 1372	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑍‘(𝑆‘𝑃)) ∈ (Base‘𝑅))
24	20, 23	eqeltrd 2833	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅))
25	6	adantr 484	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑅 ∈ Ring)
26	7, 11	cofipsgn 20409	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝)))
27	10, 26	sylan 583	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) = (𝑍‘(𝑆‘𝑝)))
28		simpllr 776	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑁 ∈ Fin)
29		simpr 488	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑝 ∈ 𝐺)
30	7, 11, 21	zrhpsgnelbas 20410	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅))
31	25, 28, 29, 30	syl3anc 1372	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘𝑝)) ∈ (Base‘𝑅))
32	27, 31	eqeltrd 2833	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅))
33		eqid 2738	. . . . . 6 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
34	33, 1	mgpbas 19364	. . . . 5 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
35	33	crngmgp 19424	. . . . . 6 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
36	35	ad3antrrr 730	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd)
37		mdetpmtr.a	. . . . . . 7 ⊢ 𝐴 = (𝑁 Mat 𝑅)
38		mdetpmtr.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐴)
39		eqid 2738	. . . . . . . . 9 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
40	39, 7	symgfv 18626	. . . . . . . 8 ⊢ ((𝑝 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁)
41	40	adantll 714	. . . . . . 7 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑝‘𝑥) ∈ 𝑁)
42		simpr 488	. . . . . . 7 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁)
43		mdetpmtr1.e	. . . . . . . . 9 ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))
44		simpll 767	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CRing)
45		simp1rr 1240	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑃 ∈ 𝐺)
46		simp2 1138	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
47	39, 7	symgfv 18626	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁)
48	45, 46, 47	syl2anc 587	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃‘𝑖) ∈ 𝑁)
49		simp3 1139	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
50		simp1rl 1239	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑀 ∈ 𝐵)
51	37, 1, 38, 48, 49, 50	matecld 21177	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑃‘𝑖)𝑀𝑗) ∈ (Base‘𝑅))
52	37, 1, 38, 10, 44, 51	matbas2d 21174	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ∈ 𝐵)
53	43, 52	eqeltrid 2837	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐸 ∈ 𝐵)
54	53	ad2antrr 726	. . . . . . 7 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 ∈ 𝐵)
55	37, 1, 38, 41, 42, 54	matecld 21177	. . . . . 6 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅))
56	55	ralrimiva 3096	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑝‘𝑥)𝐸𝑥) ∈ (Base‘𝑅))
57	34, 36, 28, 56	gsummptcl 19206	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅))
58	1, 4	ringcl 19433	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅))
59	25, 32, 57, 58	syl3anc 1372	. . 3 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ (Base‘𝑅))
60		eqid 2738	. . . 4 ⊢ (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))
61	39, 7	symgbasfi 18625	. . . . 5 ⊢ (𝑁 ∈ Fin → 𝐺 ∈ Fin)
62	10, 61	syl 17	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝐺 ∈ Fin)
63		ovexd 7205	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) ∈ V)
64		fvexd 6689	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (0g‘𝑅) ∈ V)
65	60, 62, 63, 64	fsuppmptdm 8917	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) finSupp (0g‘𝑅))
66	1, 2, 3, 4, 6, 9, 24, 59, 65	gsummulc2 19479	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))))
67		nfcv 2899	. . . 4 ⊢ Ⅎ𝑞(((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))
68		fveq2 6674	. . . . 5 ⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑍 ∘ 𝑆)‘𝑞) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)))
69		fveq1 6673	. . . . . . . 8 ⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑞‘𝑥) = ((𝑃 ∘ 𝑝)‘𝑥))
70	69	oveq1d 7185	. . . . . . 7 ⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((𝑞‘𝑥)𝑀𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))
71	70	mpteq2dv 5126	. . . . . 6 ⊢ (𝑞 = (𝑃 ∘ 𝑝) → (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))
72	71	oveq2d 7186	. . . . 5 ⊢ (𝑞 = (𝑃 ∘ 𝑝) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))
73	68, 72	oveq12d 7188	. . . 4 ⊢ (𝑞 = (𝑃 ∘ 𝑝) → (((𝑍 ∘ 𝑆)‘𝑞) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))
74		ringcmn 19453	. . . . 5 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
75	6, 74	syl 17	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑅 ∈ CMnd)
76		ssidd 3900	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (Base‘𝑅) ⊆ (Base‘𝑅))
77	6	adantr 484	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑅 ∈ Ring)
78	7, 11	cofipsgn 20409	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞)))
79	10, 78	sylan 583	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) = (𝑍‘(𝑆‘𝑞)))
80		simpllr 776	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑁 ∈ Fin)
81		simpr 488	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑞 ∈ 𝐺)
82	7, 11, 21	zrhpsgnelbas 20410	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅))
83	77, 80, 81, 82	syl3anc 1372	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (𝑍‘(𝑆‘𝑞)) ∈ (Base‘𝑅))
84	79, 83	eqeltrd 2833	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅))
85	35	ad3antrrr 730	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (mulGrp‘𝑅) ∈ CMnd)
86	39, 7	symgfv 18626	. . . . . . . . 9 ⊢ ((𝑞 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁)
87	86	adantll 714	. . . . . . . 8 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (𝑞‘𝑥) ∈ 𝑁)
88		simpr 488	. . . . . . . 8 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁)
89		simprl 771	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑀 ∈ 𝐵)
90	89	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝑀 ∈ 𝐵)
91	37, 1, 38, 87, 88, 90	matecld 21177	. . . . . . 7 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅))
92	91	ralrimiva 3096	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∀𝑥 ∈ 𝑁 ((𝑞‘𝑥)𝑀𝑥) ∈ (Base‘𝑅))
93	34, 85, 80, 92	gsummptcl 19206	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅))
94	1, 4	ringcl 19433	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ ((𝑍 ∘ 𝑆)‘𝑞) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥))) ∈ (Base‘𝑅)) → (((𝑍 ∘ 𝑆)‘𝑞) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅))
95	77, 84, 93, 94	syl3anc 1372	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑞) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))) ∈ (Base‘𝑅))
96		eqid 2738	. . . . . . 7 ⊢ (+g‘(SymGrp‘𝑁)) = (+g‘(SymGrp‘𝑁))
97	39, 7, 96	symgov 18630	. . . . . 6 ⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) = (𝑃 ∘ 𝑝))
98	39, 7, 96	symgcl 18631	. . . . . 6 ⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃(+g‘(SymGrp‘𝑁))𝑝) ∈ 𝐺)
99	97, 98	eqeltrrd 2834	. . . . 5 ⊢ ((𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺)
100	15, 99	sylan 583	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑃 ∘ 𝑝) ∈ 𝐺)
101	15	adantr 484	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → 𝑃 ∈ 𝐺)
102	7	symgfcoeu 30928	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝))
103	80, 101, 81, 102	syl3anc 1372	. . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑞 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑞 = (𝑃 ∘ 𝑝))
104	67, 1, 2, 73, 75, 62, 76, 95, 100, 103	gsummptf1o 19202	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))))
105		mdetpmtr.d	. . . . 5 ⊢ 𝐷 = (𝑁 maDet 𝑅)
106	105, 37, 38, 7, 21, 11, 4, 33	mdetleib 21338	. . . 4 ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))))
107	106	ad2antrl 728	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑞 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑞) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑞‘𝑥)𝑀𝑥)))))))
108	24	adantr 484	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅))
109	1, 4	ringass 19436	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (((𝑍 ∘ 𝑆)‘𝑃) ∈ (Base‘𝑅) ∧ ((𝑍 ∘ 𝑆)‘𝑝) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) ∈ (Base‘𝑅))) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))
110	25, 108, 32, 57, 109	syl13anc 1373	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))
111	20	adantr 484	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘𝑃) = (𝑍‘(𝑆‘𝑃)))
112	111, 27	oveq12d 7188	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))))
113	7, 11	cofipsgn 20409	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ (𝑃 ∘ 𝑝) ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))))
114	28, 100, 113	syl2anc 587	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) = (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))))
115	15	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑃 ∈ 𝐺)
116	39, 11, 7	psgnco 20399	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝)))
117	28, 115, 29, 116	syl3anc 1372	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘(𝑃 ∘ 𝑝)) = ((𝑆‘𝑃) · (𝑆‘𝑝)))
118	117	fveq2d 6678	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘(𝑆‘(𝑃 ∘ 𝑝))) = (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))))
119	21	zrhrhm 20332	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑍 ∈ (ℤring RingHom 𝑅))
120	6, 119	syl 17	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → 𝑍 ∈ (ℤring RingHom 𝑅))
121	120	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → 𝑍 ∈ (ℤring RingHom 𝑅))
122		1z 12093	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
123		neg1z 12099	. . . . . . . . . . . 12 ⊢ -1 ∈ ℤ
124		prssi 4709	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆ ℤ)
125	122, 123, 124	mp2an 692	. . . . . . . . . . 11 ⊢ {1, -1} ⊆ ℤ
126	7, 11	psgnran 18761	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1})
127	28, 115, 126	syl2anc 587	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ {1, -1})
128	125, 127	sseldi 3875	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑃) ∈ ℤ)
129	7, 11	psgnran 18761	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1})
130	10, 129	sylan 583	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ {1, -1})
131	125, 130	sseldi 3875	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑆‘𝑝) ∈ ℤ)
132		zringbas 20295	. . . . . . . . . . 11 ⊢ ℤ = (Base‘ℤring)
133		zringmulr 20298	. . . . . . . . . . 11 ⊢ · = (.r‘ℤring)
134	132, 133, 4	rhmmul 19601	. . . . . . . . . 10 ⊢ ((𝑍 ∈ (ℤring RingHom 𝑅) ∧ (𝑆‘𝑃) ∈ ℤ ∧ (𝑆‘𝑝) ∈ ℤ) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))))
135	121, 128, 131, 134	syl3anc 1372	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑍‘((𝑆‘𝑃) · (𝑆‘𝑝))) = ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))))
136	114, 118, 135	3eqtrrd 2778	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((𝑍‘(𝑆‘𝑃)) · (𝑍‘(𝑆‘𝑝))) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)))
137	112, 136	eqtrd 2773	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) = ((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)))
138	43	a1i 11	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)))
139		simprl 771	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑖 = (𝑝‘𝑥))
140	139	fveq2d 6678	. . . . . . . . . . . 12 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = (𝑃‘(𝑝‘𝑥)))
141		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑝 ∈ 𝐺)
142	39, 7	symgbasf 18622	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ 𝐺 → 𝑝:𝑁⟶𝑁)
143		ffun 6507	. . . . . . . . . . . . . 14 ⊢ (𝑝:𝑁⟶𝑁 → Fun 𝑝)
144	141, 142, 143	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → Fun 𝑝)
145		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ 𝑁)
146		fdm 6513	. . . . . . . . . . . . . . 15 ⊢ (𝑝:𝑁⟶𝑁 → dom 𝑝 = 𝑁)
147	141, 142, 146	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → dom 𝑝 = 𝑁)
148	145, 147	eleqtrrd 2836	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑥 ∈ dom 𝑝)
149		fvco 6766	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑝 ∧ 𝑥 ∈ dom 𝑝) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥)))
150	144, 148, 149	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃 ∘ 𝑝)‘𝑥) = (𝑃‘(𝑝‘𝑥)))
151	140, 150	eqtr4d 2776	. . . . . . . . . . 11 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → (𝑃‘𝑖) = ((𝑃 ∘ 𝑝)‘𝑥))
152		simprr 773	. . . . . . . . . . 11 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → 𝑗 = 𝑥)
153	151, 152	oveq12d 7188	. . . . . . . . . 10 ⊢ ((((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) ∧ (𝑖 = (𝑝‘𝑥) ∧ 𝑗 = 𝑥)) → ((𝑃‘𝑖)𝑀𝑗) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))
154		ovexd 7205	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥) ∈ V)
155	138, 153, 41, 42, 154	ovmpod 7317	. . . . . . . . 9 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) ∧ 𝑥 ∈ 𝑁) → ((𝑝‘𝑥)𝐸𝑥) = (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))
156	155	mpteq2dva 5125	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)) = (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))
157	156	oveq2d 7186	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))
158	137, 157	oveq12d 7188	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → ((((𝑍 ∘ 𝑆)‘𝑃) · ((𝑍 ∘ 𝑆)‘𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))
159	110, 158	eqtr3d 2775	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) ∧ 𝑝 ∈ 𝐺) → (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))) = (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))
160	159	mpteq2dva 5125	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))) = (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥))))))
161	160	oveq2d 7186	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘(𝑃 ∘ 𝑝)) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (((𝑃 ∘ 𝑝)‘𝑥)𝑀𝑥)))))))
162	104, 107, 161	3eqtr4d 2783	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑃) · (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))))
163	105, 37, 38, 7, 21, 11, 4, 33	mdetleib 21338	. . . 4 ⊢ (𝐸 ∈ 𝐵 → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))
164	53, 163	syl 17	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝐸) = (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥)))))))
165	164	oveq2d 7186	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝑅 Σg (𝑝 ∈ 𝐺 ↦ (((𝑍 ∘ 𝑆)‘𝑝) · ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝐸𝑥))))))))
166	66, 162, 165	3eqtr4d 2783	1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  ∃!wreu 3055  Vcvv 3398   ⊆ wss 3843  {cpr 4518   ↦ cmpt 5110  dom cdm 5525   ∘ ccom 5529  Fun wfun 6333   Fn wfn 6334  ⟶wf 6335  ‘cfv 6339  (class class class)co 7170   ∈ cmpo 7172  Fincfn 8555  1c1 10616   · cmul 10620  -cneg 10949  ℤcz 12062  Basecbs 16586  +_gcplusg 16668  ._rcmulr 16669  0_gc0g 16816   Σ_g cgsu 16817  SymGrpcsymg 18613  pmSgncpsgn 18735  CMndccmn 19024  mulGrpcmgp 19358  Ringcrg 19416  CRingccrg 19417   RingHom crh 19586  ℤ_ringzring 20289  ℤRHomczrh 20320   Mat cmat 21158   maDet cmdat 21335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-addf 10694  ax-mulf 10695

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-xor 1507  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-ot 4525  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-supp 7857  df-tpos 7921  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-er 8320  df-map 8439  df-pm 8440  df-ixp 8508  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-fsupp 8907  df-sup 8979  df-oi 9047  df-card 9441  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-xnn0 12049  df-z 12063  df-dec 12180  df-uz 12325  df-rp 12473  df-fz 12982  df-fzo 13125  df-seq 13461  df-exp 13522  df-hash 13783  df-word 13956  df-lsw 14004  df-concat 14012  df-s1 14039  df-substr 14092  df-pfx 14122  df-splice 14201  df-reverse 14210  df-s2 14299  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-sets 16593  df-ress 16594  df-plusg 16681  df-mulr 16682  df-starv 16683  df-sca 16684  df-vsca 16685  df-ip 16686  df-tset 16687  df-ple 16688  df-ds 16690  df-unif 16691  df-hom 16692  df-cco 16693  df-0g 16818  df-gsum 16819  df-prds 16824  df-pws 16826  df-mre 16960  df-mrc 16961  df-acs 16963  df-mgm 17968  df-sgrp 18017  df-mnd 18028  df-mhm 18072  df-submnd 18073  df-efmnd 18150  df-grp 18222  df-minusg 18223  df-mulg 18343  df-subg 18394  df-ghm 18474  df-gim 18517  df-cntz 18565  df-oppg 18592  df-symg 18614  df-pmtr 18688  df-psgn 18737  df-cmn 19026  df-abl 19027  df-mgp 19359  df-ur 19371  df-ring 19418  df-cring 19419  df-oppr 19495  df-dvdsr 19513  df-unit 19514  df-invr 19544  df-dvr 19555  df-rnghom 19589  df-drng 19623  df-subrg 19652  df-sra 20063  df-rgmod 20064  df-cnfld 20218  df-zring 20290  df-zrh 20324  df-dsmm 20548  df-frlm 20563  df-mat 21159  df-mdet 21336

This theorem is referenced by:  mdetpmtr2  31346  mdetpmtr12  31347