Theorem mdetpmtr12

Description: The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (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 ‘ 𝑅 )
	mdetpmtr12.e	⊢ 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) )
	mdetmptr12.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mdetmptr12.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mdetmptr12.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
	mdetmptr12.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐺 )
	mdetmptr12.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐺 )
Assertion	mdetpmtr12	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐷 ‘ 𝐸 ) ) )

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		mdetpmtr12.e	⊢ 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) )
9		mdetmptr12.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
10		mdetmptr12.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
11		mdetmptr12.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
12		mdetmptr12.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐺 )
13		mdetmptr12.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐺 )
14		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
15	14	oveq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) = ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑙 ) )
16		oveq2	⊢ ( 𝑙 = 𝑗 → ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑙 ) = ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) )
17	15 16	cbvmpov	⊢ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑗 ) )
18	1 2 3 4 5 6 7 17	mdetpmtr1	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺 ) ) → ( 𝐷 ‘ 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ) ) )
19	9 10 11 12 18	syl22anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ) ) )
20		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑃 ∈ 𝐺 )
22		simp2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
23		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
24	23 4	symgfv	⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑘 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝑁 )
25	21 22 24	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝑁 )
26		simp3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
27	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
28	1 20 2 25 26 27	matecld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
29	1 20 2 10 9 28	matbas2d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ∈ 𝐵 )
30		eqid	⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) )
31	1 2 3 4 5 6 7 30	mdetpmtr2	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ ( ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ∈ 𝐵 ∧ 𝑄 ∈ 𝐺 ) ) → ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) ) ) )
32	9 10 29 13 31	syl22anc	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) ) ) )
33		simp2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
34	13	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑄 ∈ 𝐺 )
35		simp3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
36	23 4	symgfv	⊢ ( ( 𝑄 ∈ 𝐺 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑗 ) ∈ 𝑁 )
37	34 35 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑗 ) ∈ 𝑁 )
38		oveq2	⊢ ( 𝑙 = ( 𝑄 ‘ 𝑗 ) → ( ( 𝑃 ‘ 𝑖 ) 𝑀 𝑙 ) = ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) )
39		eqid	⊢ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) )
40		ovex	⊢ ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) ∈ V
41	15 38 39 40	ovmpo	⊢ ( ( 𝑖 ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑗 ) ∈ 𝑁 ) → ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) )
42	33 37 41	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) )
43	42	mpoeq3dva	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) ) )
44	8 43	eqtr4id	⊢ ( 𝜑 → 𝐸 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) )
45	44	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐸 ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) ) )
46	45	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ 𝐸 ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ( 𝑄 ‘ 𝑗 ) ) ) ) ) )
47	32 46	eqtr4d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ 𝐸 ) ) )
48	47	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑙 ) ) ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ 𝐸 ) ) ) )
49		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
50	9 49	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
51	4 5 6	zrhcopsgnelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑅 ) )
52	50 10 12 51	syl3anc	⊢ ( 𝜑 → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑅 ) )
53	4 5 6	zrhcopsgnelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) )
54	50 10 13 53	syl3anc	⊢ ( 𝜑 → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) )
55	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ 𝐺 )
56	23 4	symgfv	⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑖 ) ∈ 𝑁 )
57	55 33 56	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑖 ) ∈ 𝑁 )
58	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
59	1 20 2 57 37 58	matecld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
60	1 20 2 10 9 59	matbas2d	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑀 ( 𝑄 ‘ 𝑗 ) ) ) ∈ 𝐵 )
61	8 60	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
62	3 1 2 20	mdetcl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐸 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) )
63	9 61 62	syl2anc	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) )
64	20 7	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝐸 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ) · ( 𝐷 ‘ 𝐸 ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ 𝐸 ) ) ) )
65	50 52 54 63 64	syl13anc	⊢ ( 𝜑 → ( ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ) · ( 𝐷 ‘ 𝐸 ) ) = ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ 𝐸 ) ) ) )
66	4 5	cofipsgn	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) )
67	10 12 66	syl2anc	⊢ ( 𝜑 → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) )
68	4 5	cofipsgn	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐺 ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑄 ) ) )
69	10 13 68	syl2anc	⊢ ( 𝜑 → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑄 ) ) )
70	67 69	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ) = ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑄 ) ) ) )
71	6	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
72	50 71	syl	⊢ ( 𝜑 → 𝑍 ∈ ( ℤring RingHom 𝑅 ) )
73		1z	⊢ 1 ∈ ℤ
74		neg1z	⊢ - 1 ∈ ℤ
75		prssi	⊢ ( ( 1 ∈ ℤ ∧ - 1 ∈ ℤ ) → { 1 , - 1 } ⊆ ℤ )
76	73 74 75	mp2an	⊢ { 1 , - 1 } ⊆ ℤ
77	4 5	psgnran	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑃 ) ∈ { 1 , - 1 } )
78	10 12 77	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ { 1 , - 1 } )
79	76 78	sseldi	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ℤ )
80	4 5	psgnran	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐺 ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } )
81	10 13 80	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } )
82	76 81	sseldi	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑄 ) ∈ ℤ )
83		zringbas	⊢ ℤ = ( Base ‘ ℤring )
84		zringmulr	⊢ · = ( .r ‘ ℤring )
85	83 84 7	rhmmul	⊢ ( ( 𝑍 ∈ ( ℤring RingHom 𝑅 ) ∧ ( 𝑆 ‘ 𝑃 ) ∈ ℤ ∧ ( 𝑆 ‘ 𝑄 ) ∈ ℤ ) → ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) = ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑄 ) ) ) )
86	72 79 82 85	syl3anc	⊢ ( 𝜑 → ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) = ( ( 𝑍 ‘ ( 𝑆 ‘ 𝑃 ) ) · ( 𝑍 ‘ ( 𝑆 ‘ 𝑄 ) ) ) )
87	70 86	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ) = ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) )
88	87	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) ) · ( 𝐷 ‘ 𝐸 ) ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐷 ‘ 𝐸 ) ) )
89	65 88	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑄 ) · ( 𝐷 ‘ 𝐸 ) ) ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐷 ‘ 𝐸 ) ) )
90	19 48 89	3eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐷 ‘ 𝐸 ) ) )