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