mdetleib2

Description: Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	mdetfval.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdetfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mdetfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mdetfval.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	mdetfval.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
	mdetfval.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	mdetfval.t	⊢ · = ( ._r ‘ 𝑅 )
	mdetfval.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
Assertion	mdetleib2	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetfval.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetfval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mdetfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mdetfval.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5		mdetfval.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
6		mdetfval.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
7		mdetfval.t	⊢ · = ( ._r ‘ 𝑅 )
8		mdetfval.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
9	1 2 3 4 5 6 7 8	mdetleib	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ) )
10	9	adantl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ) )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
13		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
14	12 13	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CMnd )
15	14	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
16	2 3	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
17	16	adantl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
18	17	simpld	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
19		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
20	19 4	symgbasfi	⊢ ( 𝑁 ∈ Fin → 𝑃 ∈ Fin )
21	18 20	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Fin )
22	12	ad2antrr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑅 ∈ Ring )
23	5 6	coeq12i	⊢ ( 𝑌 ∘ 𝑆 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) )
24		zrhpsgnmhm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
25	23 24	eqeltrid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑌 ∘ 𝑆 ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
26	12 18 25	syl2an2r	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑌 ∘ 𝑆 ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
27		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
28	27 11	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
29	4 28	mhmf	⊢ ( ( 𝑌 ∘ 𝑆 ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( 𝑌 ∘ 𝑆 ) : 𝑃 ⟶ ( Base ‘ 𝑅 ) )
30	26 29	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑌 ∘ 𝑆 ) : 𝑃 ⟶ ( Base ‘ 𝑅 ) )
31	30	ffvelrnda	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) ∈ ( Base ‘ 𝑅 ) )
32	8 11	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑈 )
33	8	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝑈 ∈ CMnd )
34	33	ad2antrr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑈 ∈ CMnd )
35	18	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑁 ∈ Fin )
36		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
37	2 11 3	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑_m ( 𝑁 × 𝑁 ) ) )
38		elmapi	⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑_m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
39	36 37 38	3syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
40	39	ad2antrr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
41	19 4	symgbasf1o	⊢ ( 𝑞 ∈ 𝑃 → 𝑞 : 𝑁 –1-1-onto→ 𝑁 )
42	41	adantl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑞 : 𝑁 –1-1-onto→ 𝑁 )
43		f1of	⊢ ( 𝑞 : 𝑁 –1-1-onto→ 𝑁 → 𝑞 : 𝑁 ⟶ 𝑁 )
44	42 43	syl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑞 : 𝑁 ⟶ 𝑁 )
45	44	ffvelrnda	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( 𝑞 ‘ 𝑦 ) ∈ 𝑁 )
46		simpr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
47	40 45 46	fovrnd	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
48	47	ralrimiva	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → ∀ 𝑦 ∈ 𝑁 ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
49	32 34 35 48	gsummptcl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) )
50	11 7	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
51	22 31 49 50	syl3anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
52	51	ralrimiva	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑞 ∈ 𝑃 ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
53		eqid	⊢ ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) = ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) )
54		eqid	⊢ ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) = ( inv_g ‘ ( SymGrp ‘ 𝑁 ) )
55	19	symggrp	⊢ ( 𝑁 ∈ Fin → ( SymGrp ‘ 𝑁 ) ∈ Grp )
56	18 55	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( SymGrp ‘ 𝑁 ) ∈ Grp )
57	4 54 56	grpinvf1o	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) : 𝑃 –1-1-onto→ 𝑃 )
58	11 15 21 52 53 57	gsummptfif1o	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 Σ_g ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ) = ( 𝑅 Σ_g ( ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ∘ ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ) ) )
59		f1of	⊢ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) : 𝑃 –1-1-onto→ 𝑃 → ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) : 𝑃 ⟶ 𝑃 )
60	57 59	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) : 𝑃 ⟶ 𝑃 )
61	60	ffvelrnda	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ∈ 𝑃 )
62	60	feqmptd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) )
63		eqidd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) = ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) )
64		fveq2	⊢ ( 𝑞 = ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) = ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) )
65		fveq1	⊢ ( 𝑞 = ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) → ( 𝑞 ‘ 𝑦 ) = ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) )
66	65	oveq1d	⊢ ( 𝑞 = ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) → ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) = ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) )
67	66	mpteq2dv	⊢ ( 𝑞 = ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) → ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) = ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) )
68	67	oveq2d	⊢ ( 𝑞 = ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) → ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) = ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) )
69	64 68	oveq12d	⊢ ( 𝑞 = ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) )
70	61 62 63 69	fmptco	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ∘ ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) )
71	19 4 54	symginv	⊢ ( 𝑝 ∈ 𝑃 → ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) = ^◡ 𝑝 )
72	71	adantl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) = ^◡ 𝑝 )
73	72	fveq2d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ ^◡ 𝑝 ) )
74	12	ad2antrr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑅 ∈ Ring )
75	18	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑁 ∈ Fin )
76		simpr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
77	4 5 6	zrhpsgninv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ^◡ 𝑝 ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) )
78	74 75 76 77	syl3anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ^◡ 𝑝 ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) )
79	73 78	eqtrd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) )
80		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
81	33	ad2antrr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑈 ∈ CMnd )
82	39	ad2antrr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
83	71	ad2antlr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) = ^◡ 𝑝 )
84	83	fveq1d	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) = ( ^◡ 𝑝 ‘ 𝑦 ) )
85	19 4	symgbasf1o	⊢ ( 𝑝 ∈ 𝑃 → 𝑝 : 𝑁 –1-1-onto→ 𝑁 )
86	85	adantl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 : 𝑁 –1-1-onto→ 𝑁 )
87		f1ocnv	⊢ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 → ^◡ 𝑝 : 𝑁 –1-1-onto→ 𝑁 )
88		f1of	⊢ ( ^◡ 𝑝 : 𝑁 –1-1-onto→ 𝑁 → ^◡ 𝑝 : 𝑁 ⟶ 𝑁 )
89	86 87 88	3syl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ^◡ 𝑝 : 𝑁 ⟶ 𝑁 )
90	89	ffvelrnda	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ^◡ 𝑝 ‘ 𝑦 ) ∈ 𝑁 )
91	84 90	eqeltrd	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) ∈ 𝑁 )
92		simpr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
93	82 91 92	fovrnd	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
94	93 32	eleqtrdi	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑁 ) → ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ∈ ( Base ‘ 𝑈 ) )
95	94	ralrimiva	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ∀ 𝑦 ∈ 𝑁 ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ∈ ( Base ‘ 𝑈 ) )
96		eqid	⊢ ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) = ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) )
97	80 81 75 95 96 86	gsummptfif1o	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) = ( 𝑈 Σ_g ( ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ∘ 𝑝 ) ) )
98		f1of	⊢ ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 → 𝑝 : 𝑁 ⟶ 𝑁 )
99	86 98	syl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 : 𝑁 ⟶ 𝑁 )
100	99	ffvelrnda	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑥 ) ∈ 𝑁 )
101	99	feqmptd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 = ( 𝑥 ∈ 𝑁 ↦ ( 𝑝 ‘ 𝑥 ) ) )
102		eqidd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) = ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) )
103		fveq2	⊢ ( 𝑦 = ( 𝑝 ‘ 𝑥 ) → ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) = ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) )
104		id	⊢ ( 𝑦 = ( 𝑝 ‘ 𝑥 ) → 𝑦 = ( 𝑝 ‘ 𝑥 ) )
105	103 104	oveq12d	⊢ ( 𝑦 = ( 𝑝 ‘ 𝑥 ) → ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) = ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) 𝑀 ( 𝑝 ‘ 𝑥 ) ) )
106	100 101 102 105	fmptco	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ∘ 𝑝 ) = ( 𝑥 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) )
107	71	ad2antlr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) = ^◡ 𝑝 )
108	107	fveq1d	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) = ( ^◡ 𝑝 ‘ ( 𝑝 ‘ 𝑥 ) ) )
109		f1ocnvfv1	⊢ ( ( 𝑝 : 𝑁 –1-1-onto→ 𝑁 ∧ 𝑥 ∈ 𝑁 ) → ( ^◡ 𝑝 ‘ ( 𝑝 ‘ 𝑥 ) ) = 𝑥 )
110	86 109	sylan	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑁 ) → ( ^◡ 𝑝 ‘ ( 𝑝 ‘ 𝑥 ) ) = 𝑥 )
111	108 110	eqtrd	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) = 𝑥 )
112	111	oveq1d	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) 𝑀 ( 𝑝 ‘ 𝑥 ) ) = ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) )
113	112	mpteq2dva	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ ( 𝑝 ‘ 𝑥 ) ) 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) )
114	106 113	eqtrd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ∘ 𝑝 ) = ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) )
115	114	oveq2d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑈 Σ_g ( ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ∘ 𝑝 ) ) = ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) )
116	97 115	eqtrd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) = ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) )
117	79 116	oveq12d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) ) )
118	117	mpteq2dva	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( ( ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ‘ 𝑝 ) ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) ) ) )
119	70 118	eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ∘ ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ) = ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) ) ) )
120	119	oveq2d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 Σ_g ( ( 𝑞 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑞 ) · ( 𝑈 Σ_g ( 𝑦 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑦 ) 𝑀 𝑦 ) ) ) ) ) ∘ ( inv_g ‘ ( SymGrp ‘ 𝑁 ) ) ) ) = ( 𝑅 Σ_g ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) ) ) ) )
121	10 58 120	3eqtrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑝 ∈ 𝑃 ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) · ( 𝑈 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( 𝑥 𝑀 ( 𝑝 ‘ 𝑥 ) ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem mdetleib2

Proof