Metamath Proof Explorer

Theorem mdetpmtr1

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)

Ref Expression
Hypotheses 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 mdetpmtr1 ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 mdetpmtr.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mdetpmtr.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mdetpmtr.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
4 mdetpmtr.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5 mdetpmtr.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
6 mdetpmtr.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
7 mdetpmtr.t ⊢ · = ( .r ‘ 𝑅 )
8 mdetpmtr1.e ⊢ 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
12 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
13 12 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑅 ∈ Ring )
14 4 fvexi ⊢ 𝐺 ∈ V
15 14 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝐺 ∈ V )
16 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑁 ∈ Fin )
17 5 4 psgndmfi ⊢ ( 𝑁 ∈ Fin → 𝑆 Fn 𝐺 )
18 fnfun ⊢ ( 𝑆 Fn 𝐺 → Fun 𝑆 )
19 16 17 18 3syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → Fun 𝑆 )
20 simprr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑃 ∈ 𝐺 )
21 fndm ⊢ ( 𝑆 Fn 𝐺 → dom 𝑆 = 𝐺 )
22 16 17 21 3syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → dom 𝑆 = 𝐺 )
23 20 22 eleqtrrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑃 ∈ dom 𝑆 )
24 fvco ⊢ ( ( Fun 𝑆 ∧ 𝑃 ∈ dom 𝑆 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) )
25 19 23 24 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) )
26 4 5 6 zrhpsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝑅 ) )
27 13 16 20 26 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝑅 ) )
28 25 27 eqeltrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑅 ) )
29 13 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → 𝑅 ∈ Ring )
30 4 5 cofipsgn ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) )
31 16 30 sylan ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) )
32 simpllr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → 𝑁 ∈ Fin )
33 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → 𝑝 ∈ 𝐺 )
34 4 5 6 zrhpsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺 ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) ∈ ( Base ‘ 𝑅 ) )
35 29 32 33 34 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) ∈ ( Base ‘ 𝑅 ) )
36 31 35 eqeltrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) )
37 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
38 37 9 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
39 37 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
40 39 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
41 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
42 41 4 symgfv ⊢ ( ( 𝑝 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑥 ) ∈ 𝑁 )
43 42 adantll ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → ( 𝑝 ‘ 𝑥 ) ∈ 𝑁 )
44 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
45 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑅 ∈ CRing )
46 simp1rr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ 𝐺 )
47 simp2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
48 41 4 symgfv ⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑖 ) ∈ 𝑁 )
49 46 47 48 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑖 ) ∈ 𝑁 )
50 simp3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
51 simp1rl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
52 1 9 2 49 50 51 matecld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
53 1 9 2 16 45 52 matbas2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) ) ∈ 𝐵 )
54 8 53 eqeltrid ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝐸 ∈ 𝐵 )
55 54 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → 𝐸 ∈ 𝐵 )
56 1 9 2 43 44 55 matecld ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
57 56 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ∀ 𝑥 ∈ 𝑁 ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
58 38 40 32 57 gsummptcl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
59 9 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
60 29 36 58 59 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
61 eqid ⊢ ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) = ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) )
62 41 4 symgbasfi ⊢ ( 𝑁 ∈ Fin → 𝐺 ∈ Fin )
63 16 62 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝐺 ∈ Fin )
64 ovexd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ∈ V )
65 fvexd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
66 61 63 64 65 fsuppmptdm ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
67 9 10 11 7 13 15 28 60 66 gsummulc2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) ) )
68 nfcv ⊢ Ⅎ 𝑞 ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) )
69 fveq2 ⊢ ( 𝑞 = ( 𝑃 ∘ 𝑝 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) = ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) )
70 fveq1 ⊢ ( 𝑞 = ( 𝑃 ∘ 𝑝 ) → ( 𝑞 ‘ 𝑥 ) = ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) )
71 70 oveq1d ⊢ ( 𝑞 = ( 𝑃 ∘ 𝑝 ) → ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) = ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) )
72 71 mpteq2dv ⊢ ( 𝑞 = ( 𝑃 ∘ 𝑝 ) → ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) )
73 72 oveq2d ⊢ ( 𝑞 = ( 𝑃 ∘ 𝑝 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) )
74 69 73 oveq12d ⊢ ( 𝑞 = ( 𝑃 ∘ 𝑝 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) )
75 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
76 13 75 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑅 ∈ CMnd )
77 ssidd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
78 13 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → 𝑅 ∈ Ring )
79 4 5 cofipsgn ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑞 ) ) )
80 16 79 sylan ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑞 ) ) )
81 simpllr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → 𝑁 ∈ Fin )
82 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → 𝑞 ∈ 𝐺 )
83 4 5 6 zrhpsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑞 ∈ 𝐺 ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑞 ) ) ∈ ( Base ‘ 𝑅 ) )
84 78 81 82 83 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑞 ) ) ∈ ( Base ‘ 𝑅 ) )
85 80 84 eqeltrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) ∈ ( Base ‘ 𝑅 ) )
86 39 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
87 41 4 symgfv ⊢ ( ( 𝑞 ∈ 𝐺 ∧ 𝑥 ∈ 𝑁 ) → ( 𝑞 ‘ 𝑥 ) ∈ 𝑁 )
88 87 adantll ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → ( 𝑞 ‘ 𝑥 ) ∈ 𝑁 )
89 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
90 simprl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑀 ∈ 𝐵 )
91 90 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
92 1 9 2 88 89 91 matecld ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
93 92 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ∀ 𝑥 ∈ 𝑁 ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
94 38 86 81 93 gsummptcl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
95 9 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
96 78 85 94 95 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
97 eqid ⊢ ( +g ‘ ( SymGrp ‘ 𝑁 ) ) = ( +g ‘ ( SymGrp ‘ 𝑁 ) )
98 41 4 97 symgov ⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺 ) → ( 𝑃 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) = ( 𝑃 ∘ 𝑝 ) )
99 41 4 97 symgcl ⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺 ) → ( 𝑃 ( +g ‘ ( SymGrp ‘ 𝑁 ) ) 𝑝 ) ∈ 𝐺 )
100 98 99 eqeltrrd ⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺 ) → ( 𝑃 ∘ 𝑝 ) ∈ 𝐺 )
101 20 100 sylan ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑃 ∘ 𝑝 ) ∈ 𝐺 )
102 20 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → 𝑃 ∈ 𝐺 )
103 4 symgfcoeu ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑞 ∈ 𝐺 ) → ∃! 𝑝 ∈ 𝐺 𝑞 = ( 𝑃 ∘ 𝑝 ) )
104 81 102 82 103 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑞 ∈ 𝐺 ) → ∃! 𝑝 ∈ 𝐺 𝑞 = ( 𝑃 ∘ 𝑝 ) )
105 68 9 10 74 76 63 77 96 101 104 gsummptf1o ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑅 Σg ( 𝑞 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )
106 3 1 2 4 6 5 7 37 mdetleib ⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑞 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )
107 106 ad2antrl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑞 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑞 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑞 ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )
108 28 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑅 ) )
109 9 7 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) )
110 29 108 36 58 109 syl13anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) )
111 25 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) )
112 111 31 oveq12d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ) = ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) ) )
113 4 5 cofipsgn ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝑃 ∘ 𝑝 ) ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) = ( 𝑍 ‘ ( 𝑆 ‘ ( 𝑃 ∘ 𝑝 ) ) ) )
114 32 101 113 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) = ( 𝑍 ‘ ( 𝑆 ‘ ( 𝑃 ∘ 𝑝 ) ) ) )
115 20 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → 𝑃 ∈ 𝐺 )
116 41 5 4 psgnco ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ ( 𝑃 ∘ 𝑝 ) ) = ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑝 ) ) )
117 32 115 33 116 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ ( 𝑃 ∘ 𝑝 ) ) = ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑝 ) ) )
118 117 fveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑍 ‘ ( 𝑆 ‘ ( 𝑃 ∘ 𝑝 ) ) ) = ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑝 ) ) ) )
119 6 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
120 13 119 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
121 120 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
122 1z ⊢ 1 ∈ ℤ
123 neg1z ⊢ - 1 ∈ ℤ
124 prssi ⊢ ( ( 1 ∈ ℤ ∧ - 1 ∈ ℤ ) → { 1 , - 1 } ⊆ ℤ )
125 122 123 124 mp2an ⊢ { 1 , - 1 } ⊆ ℤ
126 4 5 psgnran ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑃 ) ∈ { 1 , - 1 } )
127 32 115 126 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑃 ) ∈ { 1 , - 1 } )
128 125 127 sselid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑃 ) ∈ ℤ )
129 4 5 psgnran ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑝 ) ∈ { 1 , - 1 } )
130 16 129 sylan ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑝 ) ∈ { 1 , - 1 } )
131 125 130 sselid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑝 ) ∈ ℤ )
132 zringbas ⊢ ℤ = ( Base ‘ ℤring )
133 zringmulr ⊢ · = ( .r ‘ ℤring )
134 132 133 7 rhmmul ⊢ ( ( 𝑍 ∈ ( ℤring RingHom 𝑅 ) ∧ ( 𝑆 ‘ 𝑃 ) ∈ ℤ ∧ ( 𝑆 ‘ 𝑝 ) ∈ ℤ ) → ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑝 ) ) ) = ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) ) )
135 121 128 131 134 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑝 ) ) ) = ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) ) )
136 114 118 135 3eqtrrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑝 ) ) ) = ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) )
137 112 136 eqtrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ) = ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) )
138 8 a1i ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) ) )
139 simprl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → 𝑖 = ( 𝑝 ‘ 𝑥 ) )
140 139 fveq2d ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑝 ‘ 𝑥 ) ) )
141 simpllr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → 𝑝 ∈ 𝐺 )
142 41 4 symgbasf ⊢ ( 𝑝 ∈ 𝐺 → 𝑝 : 𝑁 ⟶ 𝑁 )
143 ffun ⊢ ( 𝑝 : 𝑁 ⟶ 𝑁 → Fun 𝑝 )
144 141 142 143 3syl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → Fun 𝑝 )
145 simplr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → 𝑥 ∈ 𝑁 )
146 fdm ⊢ ( 𝑝 : 𝑁 ⟶ 𝑁 → dom 𝑝 = 𝑁 )
147 141 142 146 3syl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → dom 𝑝 = 𝑁 )
148 145 147 eleqtrrd ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → 𝑥 ∈ dom 𝑝 )
149 fvco ⊢ ( ( Fun 𝑝 ∧ 𝑥 ∈ dom 𝑝 ) → ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑝 ‘ 𝑥 ) ) )
150 144 148 149 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑝 ‘ 𝑥 ) ) )
151 140 150 eqtr4d ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → ( 𝑃 ‘ 𝑖 ) = ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) )
152 simprr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → 𝑗 = 𝑥 )
153 151 152 oveq12d ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝑥 ) ∧ 𝑗 = 𝑥 ) ) → ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) = ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) )
154 ovexd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ∈ V )
155 138 153 43 44 154 ovmpod ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑁 ) → ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) = ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) )
156 155 mpteq2dva ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) )
157 156 oveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) )
158 137 157 oveq12d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) )
159 110 158 eqtr3d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) ∧ 𝑝 ∈ 𝐺 ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) )
160 159 mpteq2dva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) = ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) )
161 160 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ ( 𝑃 ∘ 𝑝 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( ( 𝑃 ∘ 𝑝 ) ‘ 𝑥 ) 𝑀 𝑥 ) ) ) ) ) ) )
162 105 107 161 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) ) )
163 3 1 2 4 6 5 7 37 mdetleib ⊢ ( 𝐸 ∈ 𝐵 → ( 𝐷 ‘ 𝐸 ) = ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) )
164 54 163 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) )
165 164 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ 𝐸 ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝑅 Σg ( 𝑝 ∈ 𝐺 ↦ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑝 ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝐸 𝑥 ) ) ) ) ) ) ) )
166 67 162 165 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ 𝐸 ) ) )