Theorem m2detleib 22017

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.)

Hypotheses

Ref	Expression
m2detleib.n	⊢ 𝑁 = {1, 2}
m2detleib.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
m2detleib.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
m2detleib.b	⊢ 𝐵 = (Base‘𝐴)
m2detleib.m	⊢ − = (-g‘𝑅)
m2detleib.t	⊢ · = (.r‘𝑅)

Assertion

Ref	Expression
m2detleib	⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2))))

Proof of Theorem m2detleib

Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		m2detleib.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
2		m2detleib.a	. . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		m2detleib.b	. . . 4 ⊢ 𝐵 = (Base‘𝐴)
4		eqid 2731	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
5		eqid 2731	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
6		eqid 2731	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
7		m2detleib.t	. . . 4 ⊢ · = (.r‘𝑅)
8		eqid 2731	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
9	1, 2, 3, 4, 5, 6, 7, 8	mdetleib1 21977	. . 3 ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))))
10	9	adantl 482	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))))
11		eqid 2731	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
12		eqid 2731	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
13		ringcmn 20017	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
14	13	adantr 481	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ CMnd)
15		m2detleib.n	. . . . . 6 ⊢ 𝑁 = {1, 2}
16		prfi 9273	. . . . . 6 ⊢ {1, 2} ∈ Fin
17	15, 16	eqeltri 2828	. . . . 5 ⊢ 𝑁 ∈ Fin
18		eqid 2731	. . . . . 6 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
19	18, 4	symgbasfi 19174	. . . . 5 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
20	17, 19	ax-mp 5	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) ∈ Fin
21	20	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) ∈ Fin)
22		simpl 483	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
23	22	adantr 481	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
24	4, 6, 5	zrhpsgnelbas 21035	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅))
25	17, 24	mp3an2 1449	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅))
26	25	adantlr 713	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅))
27		simpr 485	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑘 ∈ (Base‘(SymGrp‘𝑁)))
28		simpr 485	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵)
29	28	adantr 481	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑀 ∈ 𝐵)
30	15, 4, 2, 3, 8	m2detleiblem2 22014	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
31	23, 27, 29, 30	syl3anc 1371	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
32	11, 7	ringcl 19995	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
33	23, 26, 31, 32	syl3anc 1371	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
34		opex 5426	. . . . . . . 8 ⊢ ⟨1, 1⟩ ∈ V
35		opex 5426	. . . . . . . 8 ⊢ ⟨2, 2⟩ ∈ V
36	34, 35	pm3.2i 471	. . . . . . 7 ⊢ (⟨1, 1⟩ ∈ V ∧ ⟨2, 2⟩ ∈ V)
37		opex 5426	. . . . . . . 8 ⊢ ⟨1, 2⟩ ∈ V
38		opex 5426	. . . . . . . 8 ⊢ ⟨2, 1⟩ ∈ V
39	37, 38	pm3.2i 471	. . . . . . 7 ⊢ (⟨1, 2⟩ ∈ V ∧ ⟨2, 1⟩ ∈ V)
40	36, 39	pm3.2i 471	. . . . . 6 ⊢ ((⟨1, 1⟩ ∈ V ∧ ⟨2, 2⟩ ∈ V) ∧ (⟨1, 2⟩ ∈ V ∧ ⟨2, 1⟩ ∈ V))
41		1ne2 12370	. . . . . . . . . 10 ⊢ 1 ≠ 2
42	41	olci 864	. . . . . . . . 9 ⊢ (1 ≠ 1 ∨ 1 ≠ 2)
43		1ex 11160	. . . . . . . . . 10 ⊢ 1 ∈ V
44	43, 43	opthne 5444	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ≠ ⟨1, 2⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 2))
45	42, 44	mpbir 230	. . . . . . . 8 ⊢ ⟨1, 1⟩ ≠ ⟨1, 2⟩
46	41	orci 863	. . . . . . . . 9 ⊢ (1 ≠ 2 ∨ 1 ≠ 1)
47	43, 43	opthne 5444	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ≠ ⟨2, 1⟩ ↔ (1 ≠ 2 ∨ 1 ≠ 1))
48	46, 47	mpbir 230	. . . . . . . 8 ⊢ ⟨1, 1⟩ ≠ ⟨2, 1⟩
49	45, 48	pm3.2i 471	. . . . . . 7 ⊢ (⟨1, 1⟩ ≠ ⟨1, 2⟩ ∧ ⟨1, 1⟩ ≠ ⟨2, 1⟩)
50	49	orci 863	. . . . . 6 ⊢ ((⟨1, 1⟩ ≠ ⟨1, 2⟩ ∧ ⟨1, 1⟩ ≠ ⟨2, 1⟩) ∨ (⟨2, 2⟩ ≠ ⟨1, 2⟩ ∧ ⟨2, 2⟩ ≠ ⟨2, 1⟩))
51	40, 50	pm3.2i 471	. . . . 5 ⊢ (((⟨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⟩)))
52	51	a1i 11	. . . 4 ⊢ ((𝑅 ∈ 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⟩))))
53		prneimg 4817	. . . . 5 ⊢ (((⟨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⟩}))
54	53	imp 407	. . . 4 ⊢ ((((⟨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		disjsn2 4678	. . . 4 ⊢ ({⟨1, 1⟩, ⟨2, 2⟩} ≠ {⟨1, 2⟩, ⟨2, 1⟩} → ({{⟨1, 1⟩, ⟨2, 2⟩}} ∩ {{⟨1, 2⟩, ⟨2, 1⟩}}) = ∅)
56	52, 54, 55	3syl 18	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ({{⟨1, 1⟩, ⟨2, 2⟩}} ∩ {{⟨1, 2⟩, ⟨2, 1⟩}}) = ∅)
57		2nn 12235	. . . . . 6 ⊢ 2 ∈ ℕ
58	18, 4, 15	symg2bas 19188	. . . . . 6 ⊢ ((1 ∈ V ∧ 2 ∈ ℕ) → (Base‘(SymGrp‘𝑁)) = {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}})
59	43, 57, 58	mp2an 690	. . . . 5 ⊢ (Base‘(SymGrp‘𝑁)) = {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
60		df-pr 4594	. . . . 5 ⊢ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}} = ({{⟨1, 1⟩, ⟨2, 2⟩}} ∪ {{⟨1, 2⟩, ⟨2, 1⟩}})
61	59, 60	eqtri 2759	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = ({{⟨1, 1⟩, ⟨2, 2⟩}} ∪ {{⟨1, 2⟩, ⟨2, 1⟩}})
62	61	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = ({{⟨1, 1⟩, ⟨2, 2⟩}} ∪ {{⟨1, 2⟩, ⟨2, 1⟩}}))
63	11, 12, 14, 21, 33, 56, 62	gsummptfidmsplit 19721	. 2 ⊢ ((𝑅 ∈ 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 (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))))
64		ringmnd 19988	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
65	64	adantr 481	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd)
66		prex 5394	. . . . . 6 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ V
67	66	a1i 11	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 1⟩, ⟨2, 2⟩} ∈ V)
68	66	prid1 4728	. . . . . . . . 9 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
69	68, 59	eleqtrri 2831	. . . . . . . 8 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁))
70	69	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁)))
71	4, 6, 5	zrhpsgnelbas 21035	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) ∈ (Base‘𝑅))
72	17, 71	mp3an2 1449	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) ∈ (Base‘𝑅))
73	70, 72	sylan2 593	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) ∈ (Base‘𝑅))
74	15, 4, 2, 3, 8	m2detleiblem2 22014	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
75	69, 74	mp3an2 1449	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
76	11, 7	ringcl 19995	. . . . . 6 ⊢ ((𝑅 ∈ 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‘𝑅))
77	22, 73, 75, 76	syl3anc 1371	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
78		2fveq3 6852	. . . . . . 7 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})))
79		fveq1 6846	. . . . . . . . . 10 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑘‘𝑛) = ({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛))
80	79	oveq1d 7377	. . . . . . . . 9 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → ((𝑘‘𝑛)𝑀𝑛) = (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))
81	80	mpteq2dv 5212	. . . . . . . 8 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))
82	81	oveq2d 7378	. . . . . . 7 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))))
83	78, 82	oveq12d 7380	. . . . . 6 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))))
84	11, 83	gsumsn 19745	. . . . 5 ⊢ ((𝑅 ∈ 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⟩}‘𝑛)𝑀𝑛)))))
85	65, 67, 77, 84	syl3anc 1371	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {{⟨1, 1⟩, ⟨2, 2⟩}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))))
86		prex 5394	. . . . . 6 ⊢ {⟨1, 2⟩, ⟨2, 1⟩} ∈ V
87	86	a1i 11	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 2⟩, ⟨2, 1⟩} ∈ V)
88	86	prid2 4729	. . . . . . . . 9 ⊢ {⟨1, 2⟩, ⟨2, 1⟩} ∈ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
89	88, 59	eleqtrri 2831	. . . . . . . 8 ⊢ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁))
90	89	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁)))
91	4, 6, 5	zrhpsgnelbas 21035	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) ∈ (Base‘𝑅))
92	17, 91	mp3an2 1449	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) ∈ (Base‘𝑅))
93	90, 92	sylan2 593	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) ∈ (Base‘𝑅))
94	15, 4, 2, 3, 8	m2detleiblem2 22014	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
95	89, 94	mp3an2 1449	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
96	11, 7	ringcl 19995	. . . . . 6 ⊢ ((𝑅 ∈ 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‘𝑅))
97	22, 93, 95, 96	syl3anc 1371	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
98		2fveq3 6852	. . . . . . 7 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})))
99		fveq1 6846	. . . . . . . . . 10 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → (𝑘‘𝑛) = ({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛))
100	99	oveq1d 7377	. . . . . . . . 9 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → ((𝑘‘𝑛)𝑀𝑛) = (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))
101	100	mpteq2dv 5212	. . . . . . . 8 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))
102	101	oveq2d 7378	. . . . . . 7 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))))
103	98, 102	oveq12d 7380	. . . . . 6 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))))
104	11, 103	gsumsn 19745	. . . . 5 ⊢ ((𝑅 ∈ 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⟩}‘𝑛)𝑀𝑛)))))
105	65, 87, 97, 104	syl3anc 1371	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {{⟨1, 2⟩, ⟨2, 1⟩}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))))
106	85, 105	oveq12d 7380	. . 3 ⊢ ((𝑅 ∈ 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⟩}‘𝑛)𝑀𝑛))))))
107		eqidd 2732	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩})
108		eqid 2731	. . . . . . . 8 ⊢ (1r‘𝑅) = (1r‘𝑅)
109	15, 4, 5, 6, 108	m2detleiblem5 22011	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩}) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) = (1r‘𝑅))
110	107, 109	sylan2 593	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) = (1r‘𝑅))
111		eqidd 2732	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩})
112	8, 7	mgpplusg 19914	. . . . . . . 8 ⊢ · = (+g‘(mulGrp‘𝑅))
113	15, 4, 2, 3, 8, 112	m2detleiblem3 22015	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2)))
114	22, 111, 28, 113	syl3anc 1371	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2)))
115	110, 114	oveq12d 7380	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))) = ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))))
116	43	prid1 4728	. . . . . . . . . 10 ⊢ 1 ∈ {1, 2}
117	116, 15	eleqtrri 2831	. . . . . . . . 9 ⊢ 1 ∈ 𝑁
118	117	a1i 11	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 1 ∈ 𝑁)
119	3	eleq2i 2824	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴))
120	119	biimpi 215	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴))
121	120	adantl 482	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴))
122	2, 11	matecl 21811	. . . . . . . 8 ⊢ ((1 ∈ 𝑁 ∧ 1 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀1) ∈ (Base‘𝑅))
123	118, 118, 121, 122	syl3anc 1371	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀1) ∈ (Base‘𝑅))
124		prid2g 4727	. . . . . . . . . . 11 ⊢ (2 ∈ ℕ → 2 ∈ {1, 2})
125	57, 124	ax-mp 5	. . . . . . . . . 10 ⊢ 2 ∈ {1, 2}
126	125, 15	eleqtrri 2831	. . . . . . . . 9 ⊢ 2 ∈ 𝑁
127	126	a1i 11	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 2 ∈ 𝑁)
128	2, 11	matecl 21811	. . . . . . . 8 ⊢ ((2 ∈ 𝑁 ∧ 2 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀2) ∈ (Base‘𝑅))
129	127, 127, 121, 128	syl3anc 1371	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀2) ∈ (Base‘𝑅))
130	11, 7	ringcl 19995	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (1𝑀1) ∈ (Base‘𝑅) ∧ (2𝑀2) ∈ (Base‘𝑅)) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅))
131	22, 123, 129, 130	syl3anc 1371	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅))
132	11, 7, 108	ringlidm 20006	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2)))
133	131, 132	syldan 591	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2)))
134	115, 133	eqtrd 2771	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))) = ((1𝑀1) · (2𝑀2)))
135		eqidd 2732	. . . . . 6 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩})
136		eqid 2731	. . . . . . 7 ⊢ (invg‘𝑅) = (invg‘𝑅)
137	15, 4, 5, 6, 108, 136	m2detleiblem6 22012	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩}) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) = ((invg‘𝑅)‘(1r‘𝑅)))
138	135, 137	sylan2 593	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) = ((invg‘𝑅)‘(1r‘𝑅)))
139		eqidd 2732	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩})
140	15, 4, 2, 3, 8, 112	m2detleiblem4 22016	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2)))
141	22, 139, 28, 140	syl3anc 1371	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2)))
142	138, 141	oveq12d 7380	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))) = (((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2))))
143	134, 142	oveq12d 7380	. . 3 ⊢ ((𝑅 ∈ 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)))))
144	2, 11	matecl 21811	. . . . . 6 ⊢ ((2 ∈ 𝑁 ∧ 1 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀1) ∈ (Base‘𝑅))
145	127, 118, 121, 144	syl3anc 1371	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀1) ∈ (Base‘𝑅))
146	2, 11	matecl 21811	. . . . . 6 ⊢ ((1 ∈ 𝑁 ∧ 2 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀2) ∈ (Base‘𝑅))
147	118, 127, 121, 146	syl3anc 1371	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀2) ∈ (Base‘𝑅))
148	11, 7	ringcl 19995	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (2𝑀1) ∈ (Base‘𝑅) ∧ (1𝑀2) ∈ (Base‘𝑅)) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅))
149	22, 145, 147, 148	syl3anc 1371	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅))
150		m2detleib.m	. . . . 5 ⊢ − = (-g‘𝑅)
151	15, 4, 5, 6, 108, 136, 7, 150	m2detleiblem7 22013	. . . 4 ⊢ ((𝑅 ∈ 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	22, 131, 149, 151	syl3anc 1371	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((1𝑀1) · (2𝑀2))(+g‘𝑅)(((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2))))
153	106, 143, 152	3eqtrd 2775	. 2 ⊢ ((𝑅 ∈ 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	10, 63, 153	3eqtrd 2775	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2))))

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  Vcvv 3446   ∪ cun 3911   ∩ cin 3912  ∅c0 4287  {csn 4591  {cpr 4593  ⟨cop 4597   ↦ cmpt 5193  ‘cfv 6501  (class class class)co 7362  Fincfn 8890  1c1 11061  ℕcn 12162  2c2 12217  Basecbs 17094  +_gcplusg 17147  ._rcmulr 17148   Σ_g cgsu 17336  Mndcmnd 18570  inv_gcminusg 18763  -_gcsg 18764  SymGrpcsymg 19162  pmSgncpsgn 19285  CMndccmn 19576  mulGrpcmgp 19910  1_rcur 19927  Ringcrg 19978  ℤRHomczrh 20937   Mat cmat 21791   maDet cmdat 21970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137  ax-addf 11139  ax-mulf 11140

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-xor 1510  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-ot 4600  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-sup 9387  df-oi 9455  df-dju 9846  df-card 9884  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12423  df-xnn0 12495  df-z 12509  df-dec 12628  df-uz 12773  df-rp 12925  df-fz 13435  df-fzo 13578  df-seq 13917  df-exp 13978  df-fac 14184  df-bc 14213  df-hash 14241  df-word 14415  df-lsw 14463  df-concat 14471  df-s1 14496  df-substr 14541  df-pfx 14571  df-splice 14650  df-reverse 14659  df-s2 14749  df-struct 17030  df-sets 17047  df-slot 17065  df-ndx 17077  df-base 17095  df-ress 17124  df-plusg 17160  df-mulr 17161  df-starv 17162  df-sca 17163  df-vsca 17164  df-ip 17165  df-tset 17166  df-ple 17167  df-ds 17169  df-unif 17170  df-hom 17171  df-cco 17172  df-0g 17337  df-gsum 17338  df-prds 17343  df-pws 17345  df-mre 17480  df-mrc 17481  df-acs 17483  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-mhm 18615  df-submnd 18616  df-efmnd 18693  df-grp 18765  df-minusg 18766  df-sbg 18767  df-mulg 18887  df-subg 18939  df-ghm 19020  df-gim 19063  df-cntz 19111  df-oppg 19138  df-symg 19163  df-pmtr 19238  df-psgn 19287  df-cmn 19578  df-abl 19579  df-mgp 19911  df-ur 19928  df-ring 19980  df-cring 19981  df-rnghom 20162  df-subrg 20268  df-sra 20692  df-rgmod 20693  df-cnfld 20834  df-zring 20907  df-zrh 20941  df-dsmm 21175  df-frlm 21190  df-mat 21792  df-mdet 21971

This theorem is referenced by:  lmat22det  32492