Metamath Proof Explorer


Theorem m2detleib

Description: Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018) (Revised by AV, 26-Dec-2018) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses m2detleib.n 𝑁 = { 1 , 2 }
m2detleib.d 𝐷 = ( 𝑁 maDet 𝑅 )
m2detleib.a 𝐴 = ( 𝑁 Mat 𝑅 )
m2detleib.b 𝐵 = ( Base ‘ 𝐴 )
m2detleib.m = ( -g𝑅 )
m2detleib.t · = ( .r𝑅 )
Assertion m2detleib ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝐷𝑀 ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 m2detleib.n 𝑁 = { 1 , 2 }
2 m2detleib.d 𝐷 = ( 𝑁 maDet 𝑅 )
3 m2detleib.a 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2detleib.b 𝐵 = ( Base ‘ 𝐴 )
5 m2detleib.m = ( -g𝑅 )
6 m2detleib.t · = ( .r𝑅 )
7 eqid ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
8 eqid ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
9 eqid ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
10 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11 2 3 4 7 8 9 6 10 mdetleib1 ( 𝑀𝐵 → ( 𝐷𝑀 ) = ( 𝑅 Σg ( 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) )
12 11 adantl ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝐷𝑀 ) = ( 𝑅 Σg ( 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) )
13 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ( +g𝑅 ) = ( +g𝑅 )
15 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
16 15 adantr ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑅 ∈ CMnd )
17 prfi { 1 , 2 } ∈ Fin
18 1 17 eqeltri 𝑁 ∈ Fin
19 eqid ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
20 19 7 symgbasfi ( 𝑁 ∈ Fin → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
21 18 20 ax-mp ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin
22 21 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∈ Fin )
23 simpl ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑅 ∈ Ring )
24 23 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
25 7 9 8 zrhpsgnelbas ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
26 18 25 mp3an2 ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
27 26 adantlr ( ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
28 simpr ( ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
29 simpr ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑀𝐵 )
30 29 adantr ( ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → 𝑀𝐵 )
31 1 7 3 4 10 m2detleiblem2 ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
32 24 28 30 31 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
33 13 6 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
34 24 27 32 33 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
35 opex ⟨ 1 , 1 ⟩ ∈ V
36 opex ⟨ 2 , 2 ⟩ ∈ V
37 35 36 pm3.2i ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V )
38 opex ⟨ 1 , 2 ⟩ ∈ V
39 opex ⟨ 2 , 1 ⟩ ∈ V
40 38 39 pm3.2i ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V )
41 37 40 pm3.2i ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) )
42 1ne2 1 ≠ 2
43 42 olci ( 1 ≠ 1 ∨ 1 ≠ 2 )
44 1ex 1 ∈ V
45 44 44 opthne ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ↔ ( 1 ≠ 1 ∨ 1 ≠ 2 ) )
46 43 45 mpbir ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩
47 42 orci ( 1 ≠ 2 ∨ 1 ≠ 1 )
48 44 44 opthne ( ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ↔ ( 1 ≠ 2 ∨ 1 ≠ 1 ) )
49 47 48 mpbir ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩
50 46 49 pm3.2i ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ )
51 50 orci ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) )
52 41 51 pm3.2i ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) ∧ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) )
53 52 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) ∧ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) ) )
54 prneimg ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) → ( ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ≠ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
55 54 imp ( ( ( ( ⟨ 1 , 1 ⟩ ∈ V ∧ ⟨ 2 , 2 ⟩ ∈ V ) ∧ ( ⟨ 1 , 2 ⟩ ∈ V ∧ ⟨ 2 , 1 ⟩ ∈ V ) ) ∧ ( ( ⟨ 1 , 1 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 1 , 1 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ∨ ( ⟨ 2 , 2 ⟩ ≠ ⟨ 1 , 2 ⟩ ∧ ⟨ 2 , 2 ⟩ ≠ ⟨ 2 , 1 ⟩ ) ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ≠ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
56 disjsn2 ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ≠ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∩ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ) = ∅ )
57 53 55 56 3syl ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∩ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ) = ∅ )
58 2nn 2 ∈ ℕ
59 19 7 1 symg2bas ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
60 44 58 59 mp2an ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
61 df-pr { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } = ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∪ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
62 60 61 eqtri ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∪ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
63 62 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ∪ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ) )
64 13 14 16 22 34 57 63 gsummptfidmsplit ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ) )
65 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
66 65 adantr ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑅 ∈ Mnd )
67 prex { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V
68 67 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V )
69 67 prid1 { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
70 69 60 eleqtrri { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
71 70 a1i ( 𝑀𝐵 → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
72 7 9 8 zrhpsgnelbas ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
73 18 72 mp3an2 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
74 71 73 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
75 1 7 3 4 10 m2detleiblem2 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
76 70 75 mp3an2 ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
77 13 6 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
78 23 74 76 77 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
79 2fveq3 ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) )
80 fveq1 ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑘𝑛 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) )
81 80 oveq1d ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( 𝑘𝑛 ) 𝑀 𝑛 ) = ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) )
82 81 mpteq2dv ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) )
83 82 oveq2d ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) )
84 79 83 oveq12d ( 𝑘 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
85 13 84 gsumsn ( ( 𝑅 ∈ Mnd ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V ∧ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
86 66 68 78 85 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
87 prex { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
88 87 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V )
89 87 prid2 { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
90 89 60 eleqtrri { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
91 90 a1i ( 𝑀𝐵 → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
92 7 9 8 zrhpsgnelbas ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
93 18 92 mp3an2 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
94 91 93 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) )
95 1 7 3 4 10 m2detleiblem2 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
96 90 95 mp3an2 ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )
97 13 6 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
98 23 94 96 97 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
99 2fveq3 ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) )
100 fveq1 ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑘𝑛 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) )
101 100 oveq1d ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( 𝑘𝑛 ) 𝑀 𝑛 ) = ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) )
102 101 mpteq2dv ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) )
103 102 oveq2d ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) )
104 99 103 oveq12d ( 𝑘 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
105 13 104 gsumsn ( ( 𝑅 ∈ Mnd ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V ∧ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
106 66 88 98 105 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) )
107 86 106 oveq12d ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ( +g𝑅 ) ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) )
108 eqidd ( 𝑀𝐵 → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
109 eqid ( 1r𝑅 ) = ( 1r𝑅 )
110 1 7 8 9 109 m2detleiblem5 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) = ( 1r𝑅 ) )
111 108 110 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) = ( 1r𝑅 ) )
112 eqidd ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } )
113 10 6 mgpplusg · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
114 1 7 3 4 10 113 m2detleiblem3 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
115 23 112 29 114 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
116 111 115 oveq12d ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( 1r𝑅 ) · ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ) )
117 44 prid1 1 ∈ { 1 , 2 }
118 117 1 eleqtrri 1 ∈ 𝑁
119 118 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 1 ∈ 𝑁 )
120 4 eleq2i ( 𝑀𝐵𝑀 ∈ ( Base ‘ 𝐴 ) )
121 120 biimpi ( 𝑀𝐵𝑀 ∈ ( Base ‘ 𝐴 ) )
122 121 adantl ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
123 3 13 matecl ( ( 1 ∈ 𝑁 ∧ 1 ∈ 𝑁𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 1 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
124 119 119 122 123 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 1 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
125 prid2g ( 2 ∈ ℕ → 2 ∈ { 1 , 2 } )
126 58 125 ax-mp 2 ∈ { 1 , 2 }
127 126 1 eleqtrri 2 ∈ 𝑁
128 127 a1i ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → 2 ∈ 𝑁 )
129 3 13 matecl ( ( 2 ∈ 𝑁 ∧ 2 ∈ 𝑁𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 2 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
130 128 128 122 129 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 2 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
131 13 6 ringcl ( ( 𝑅 ∈ Ring ∧ ( 1 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 2 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
132 23 124 130 131 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
133 13 6 109 ringlidm ( ( 𝑅 ∈ Ring ∧ ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r𝑅 ) · ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
134 132 133 syldan ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 1r𝑅 ) · ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
135 116 134 eqtrd ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) )
136 eqidd ( 𝑀𝐵 → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
137 eqid ( invg𝑅 ) = ( invg𝑅 )
138 1 7 8 9 109 137 m2detleiblem6 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) = ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) )
139 136 138 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) = ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) )
140 eqidd ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
141 1 7 3 4 10 113 m2detleiblem4 ( ( 𝑅 ∈ Ring ∧ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )
142 23 140 29 141 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )
143 139 142 oveq12d ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) = ( ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
144 135 143 oveq12d ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ( +g𝑅 ) ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( +g𝑅 ) ( ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) ) )
145 3 13 matecl ( ( 2 ∈ 𝑁 ∧ 1 ∈ 𝑁𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 2 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
146 128 119 122 145 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 2 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
147 3 13 matecl ( ( 1 ∈ 𝑁 ∧ 2 ∈ 𝑁𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 1 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
148 119 128 122 147 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 1 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
149 13 6 ringcl ( ( 𝑅 ∈ Ring ∧ ( 2 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
150 23 146 148 149 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) )
151 1 7 8 9 109 137 6 5 m2detleiblem7 ( ( 𝑅 ∈ Ring ∧ ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( +g𝑅 ) ( ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
152 23 132 150 151 syl3anc ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( +g𝑅 ) ( ( ( invg𝑅 ) ‘ ( 1r𝑅 ) ) · ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
153 107 144 152 3eqtrd ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ( +g𝑅 ) ( 𝑅 Σg ( 𝑘 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( pmSgn ‘ 𝑁 ) ‘ 𝑘 ) ) · ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑛𝑁 ↦ ( ( 𝑘𝑛 ) 𝑀 𝑛 ) ) ) ) ) ) ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )
154 12 64 153 3eqtrd ( ( 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝐷𝑀 ) = ( ( ( 1 𝑀 1 ) · ( 2 𝑀 2 ) ) ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) ) )