This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdetdiaglem

Description: Lemma for mdetdiag . Previously part of proof for mdet1 . (Contributed by SO, 10-Jul-2018) (Revised by AV, 17-Aug-2019)

Ref Expression
Hypotheses mdetdiag.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetdiag.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetdiag.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetdiag.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
mdetdiag.0 ⊢ 0 = ( 0g ‘ 𝑅 )
mdetdiaglem.g ⊢ 𝐻 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
mdetdiaglem.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
mdetdiaglem.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
mdetdiaglem.t ⊢ · = ( .r ‘ 𝑅 )
Assertion mdetdiaglem ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 mdetdiag.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetdiag.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 mdetdiag.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mdetdiag.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
5 mdetdiag.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 mdetdiaglem.g ⊢ 𝐻 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
7 mdetdiaglem.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
8 mdetdiaglem.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
9 mdetdiaglem.t ⊢ · = ( .r ‘ 𝑅 )
10 7 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → 𝑍 = ( ℤRHom ‘ 𝑅 ) )
11 8 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → 𝑆 = ( pmSgn ‘ 𝑁 ) )
12 10 11 coeq12d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( 𝑍 ∘ 𝑆 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) )
13 12 fveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) )
14 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
15 14 6 symgbasf1o ⊢ ( 𝑃 ∈ 𝐻 → 𝑃 : 𝑁 –1-1-onto→ 𝑁 )
16 f1ofn ⊢ ( 𝑃 : 𝑁 –1-1-onto→ 𝑁 → 𝑃 Fn 𝑁 )
17 15 16 syl ⊢ ( 𝑃 ∈ 𝐻 → 𝑃 Fn 𝑁 )
18 fnnfpeq0 ⊢ ( 𝑃 Fn 𝑁 → ( dom ( 𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁 ) ) )
19 17 18 syl ⊢ ( 𝑃 ∈ 𝐻 → ( dom ( 𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁 ) ) )
20 19 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( dom ( 𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁 ) ) )
21 20 bicomd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑃 = ( I ↾ 𝑁 ) ↔ dom ( 𝑃 ∖ I ) = ∅ ) )
22 21 necon3bid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑃 ≠ ( I ↾ 𝑁 ) ↔ dom ( 𝑃 ∖ I ) ≠ ∅ ) )
23 n0 ⊢ ( dom ( 𝑃 ∖ I ) ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ dom ( 𝑃 ∖ I ) )
24 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
25 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26 4 25 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 )
27 4 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
28 27 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ CMnd )
29 28 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝐺 ∈ CMnd )
30 simpll2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑁 ∈ Fin )
31 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32 2 31 3 matbas2i ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
33 32 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
34 elmapi ⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
35 33 34 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
36 4 31 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
37 36 eqcomi ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑅 )
38 37 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑅 ) )
39 38 feq3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝐺 ) ↔ 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) ) )
40 35 39 mpbird ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝐺 ) )
41 40 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝐺 ) )
42 14 6 symgbasf ⊢ ( 𝑃 ∈ 𝐻 → 𝑃 : 𝑁 ⟶ 𝑁 )
43 42 ad2antrl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑃 : 𝑁 ⟶ 𝑁 )
44 43 ffvelcdmda ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝑁 )
45 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
46 41 44 45 fovcdmd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
47 disjdif ⊢ ( { 𝑠 } ∩ ( 𝑁 ∖ { 𝑠 } ) ) = ∅
48 47 a1i ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( { 𝑠 } ∩ ( 𝑁 ∖ { 𝑠 } ) ) = ∅ )
49 difss ⊢ ( 𝑃 ∖ I ) ⊆ 𝑃
50 dmss ⊢ ( ( 𝑃 ∖ I ) ⊆ 𝑃 → dom ( 𝑃 ∖ I ) ⊆ dom 𝑃 )
51 49 50 ax-mp ⊢ dom ( 𝑃 ∖ I ) ⊆ dom 𝑃
52 42 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → 𝑃 : 𝑁 ⟶ 𝑁 )
53 51 52 fssdm ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → dom ( 𝑃 ∖ I ) ⊆ 𝑁 )
54 53 sseld ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑠 ∈ dom ( 𝑃 ∖ I ) → 𝑠 ∈ 𝑁 ) )
55 54 impr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑠 ∈ 𝑁 )
56 55 snssd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → { 𝑠 } ⊆ 𝑁 )
57 undif ⊢ ( { 𝑠 } ⊆ 𝑁 ↔ ( { 𝑠 } ∪ ( 𝑁 ∖ { 𝑠 } ) ) = 𝑁 )
58 56 57 sylib ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( { 𝑠 } ∪ ( 𝑁 ∖ { 𝑠 } ) ) = 𝑁 )
59 58 eqcomd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑁 = ( { 𝑠 } ∪ ( 𝑁 ∖ { 𝑠 } ) ) )
60 24 26 29 30 46 48 59 gsummptfidmsplit ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ { 𝑠 } ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) )
61 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
62 61 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝑅 ∈ Ring )
63 4 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Mnd )
64 62 63 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐺 ∈ Mnd )
65 64 3adant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
66 65 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝐺 ∈ Mnd )
67 vex ⊢ 𝑠 ∈ V
68 67 a1i ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑠 ∈ V )
69 35 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
70 43 55 ffvelcdmd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝑃 ‘ 𝑠 ) ∈ 𝑁 )
71 69 70 55 fovcdmd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) ∈ ( Base ‘ 𝑅 ) )
72 fveq2 ⊢ ( 𝑘 = 𝑠 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑠 ) )
73 id ⊢ ( 𝑘 = 𝑠 → 𝑘 = 𝑠 )
74 72 73 oveq12d ⊢ ( 𝑘 = 𝑠 → ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) = ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) )
75 36 74 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑠 } ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) )
76 66 68 71 75 syl3anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑠 } ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) )
77 simprr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑠 ∈ dom ( 𝑃 ∖ I ) )
78 17 ad2antrl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑃 Fn 𝑁 )
79 fnelnfp ⊢ ( ( 𝑃 Fn 𝑁 ∧ 𝑠 ∈ 𝑁 ) → ( 𝑠 ∈ dom ( 𝑃 ∖ I ) ↔ ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 ) )
80 78 55 79 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝑠 ∈ dom ( 𝑃 ∖ I ) ↔ ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 ) )
81 77 80 mpbid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 )
82 42 ad2antrl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑃 : 𝑁 ⟶ 𝑁 )
83 42 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → 𝑃 : 𝑁 ⟶ 𝑁 )
84 51 83 fssdm ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → dom ( 𝑃 ∖ I ) ⊆ 𝑁 )
85 84 sseld ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑠 ∈ dom ( 𝑃 ∖ I ) → 𝑠 ∈ 𝑁 ) )
86 85 impr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑠 ∈ 𝑁 )
87 82 86 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝑃 ‘ 𝑠 ) ∈ 𝑁 )
88 neeq1 ⊢ ( 𝑖 = ( 𝑃 ‘ 𝑠 ) → ( 𝑖 ≠ 𝑗 ↔ ( 𝑃 ‘ 𝑠 ) ≠ 𝑗 ) )
89 oveq1 ⊢ ( 𝑖 = ( 𝑃 ‘ 𝑠 ) → ( 𝑖 𝑀 𝑗 ) = ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑗 ) )
90 89 eqeq1d ⊢ ( 𝑖 = ( 𝑃 ‘ 𝑠 ) → ( ( 𝑖 𝑀 𝑗 ) = 0 ↔ ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑗 ) = 0 ) )
91 88 90 imbi12d ⊢ ( 𝑖 = ( 𝑃 ‘ 𝑠 ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ↔ ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑗 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑗 ) = 0 ) ) )
92 neeq2 ⊢ ( 𝑗 = 𝑠 → ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑗 ↔ ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 ) )
93 oveq2 ⊢ ( 𝑗 = 𝑠 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑗 ) = ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) )
94 93 eqeq1d ⊢ ( 𝑗 = 𝑠 → ( ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑗 ) = 0 ↔ ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 ) )
95 92 94 imbi12d ⊢ ( 𝑗 = 𝑠 → ( ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑗 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑗 ) = 0 ) ↔ ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 ) ) )
96 91 95 rspc2v ⊢ ( ( ( 𝑃 ‘ 𝑠 ) ∈ 𝑁 ∧ 𝑠 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 ) ) )
97 87 86 96 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) → ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 ) ) )
98 97 impancom ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) → ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 ) ) )
99 98 imp ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( ( 𝑃 ‘ 𝑠 ) ≠ 𝑠 → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 ) )
100 81 99 mpd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( ( 𝑃 ‘ 𝑠 ) 𝑀 𝑠 ) = 0 )
101 76 100 eqtrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑠 } ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 )
102 101 oveq1d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( ( 𝐺 Σg ( 𝑘 ∈ { 𝑠 } ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) )
103 61 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
104 103 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → 𝑅 ∈ Ring )
105 28 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → 𝐺 ∈ CMnd )
106 simpl2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → 𝑁 ∈ Fin )
107 difss ⊢ ( 𝑁 ∖ { 𝑠 } ) ⊆ 𝑁
108 ssfi ⊢ ( ( 𝑁 ∈ Fin ∧ ( 𝑁 ∖ { 𝑠 } ) ⊆ 𝑁 ) → ( 𝑁 ∖ { 𝑠 } ) ∈ Fin )
109 106 107 108 sylancl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑁 ∖ { 𝑠 } ) ∈ Fin )
110 35 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
111 83 adantr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ) → 𝑃 : 𝑁 ⟶ 𝑁 )
112 eldifi ⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) → 𝑘 ∈ 𝑁 )
113 112 adantl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ) → 𝑘 ∈ 𝑁 )
114 111 113 ffvelcdmd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝑁 )
115 110 114 113 fovcdmd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ) → ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
116 115 ralrimiva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
117 36 105 109 116 gsummptcl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
118 117 ad2ant2r ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) )
119 31 25 5 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = 0 )
120 104 118 119 syl2anc ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑠 } ) ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = 0 )
121 60 102 120 3eqtrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom ( 𝑃 ∖ I ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 )
122 121 expr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑠 ∈ dom ( 𝑃 ∖ I ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 ) )
123 122 exlimdv ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( ∃ 𝑠 𝑠 ∈ dom ( 𝑃 ∖ I ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 ) )
124 23 123 biimtrid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( dom ( 𝑃 ∖ I ) ≠ ∅ → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 ) )
125 22 124 sylbid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ∧ 𝑃 ∈ 𝐻 ) → ( 𝑃 ≠ ( I ↾ 𝑁 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 ) )
126 125 expimpd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) → ( ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 ) )
127 126 3impia ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) = 0 )
128 13 127 oveq12d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) · 0 ) )
129 3simpa ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) )
130 simpl ⊢ ( ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) → 𝑃 ∈ 𝐻 )
131 61 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑃 ∈ 𝐻 ) → 𝑅 ∈ Ring )
132 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
133 61 132 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
134 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
135 6 134 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : 𝐻 ⟶ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
136 133 135 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : 𝐻 ⟶ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
137 136 ffvelcdmda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑃 ∈ 𝐻 ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
138 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
139 138 31 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
140 139 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ 𝑅 )
141 140 9 5 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) · 0 ) = 0 )
142 131 137 141 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑃 ∈ 𝐻 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) · 0 ) = 0 )
143 129 130 142 syl2an ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) · 0 ) = 0 )
144 143 3adant2 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑃 ) · 0 ) = 0 )
145 128 144 eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ∧ ( 𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁 ) ) ) → ( ( ( 𝑍 ∘ 𝑆 ) ‘ 𝑃 ) · ( 𝐺 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑃 ‘ 𝑘 ) 𝑀 𝑘 ) ) ) ) = 0 )