Theorem m2detleib 22745

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 2765	. . . 4 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
5		eqid 2765	. . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
6		eqid 2765	. . . 4 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
7		m2detleib.t	. . . 4 ⊢ · = (.r‘𝑅)
8		eqid 2765	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
9	1, 2, 3, 4, 5, 6, 7, 8	mdetleib1 22705	. . 3 ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))))
10	9	adantl 486	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈ (Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))))
11		eqid 2765	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
12		eqid 2765	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
13		ringcmn 20353	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
14	13	adantr 485	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ CMnd)
15		m2detleib.n	. . . . . 6 ⊢ 𝑁 = {1, 2}
16		prfi 9271	. . . . . 6 ⊢ {1, 2} ∈ Fin
17	15, 16	eqeltri 2861	. . . . 5 ⊢ 𝑁 ∈ Fin
18		eqid 2765	. . . . . 6 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
19	18, 4	symgbasfi 19437	. . . . 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 487	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
23	22	adantr 485	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
24	4, 6, 5	zrhpsgnelbas 21701	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅))
25	17, 24	mp3an2 1473	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅))
26	25	adantlr 727	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅))
27		simpr 489	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑘 ∈ (Base‘(SymGrp‘𝑁)))
28		simpr 489	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵)
29	28	adantr 485	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑀 ∈ 𝐵)
30	15, 4, 2, 3, 8	m2detleiblem2 22742	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
31	23, 27, 29, 30	syl3anc 1394	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
32	11, 7	ringcl 20320	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
33	23, 26, 31, 32	syl3anc 1394	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
34		opex 5435	. . . . . . . 8 ⊢ ⟨1, 1⟩ ∈ V
35		opex 5435	. . . . . . . 8 ⊢ ⟨2, 2⟩ ∈ V
36	34, 35	pm3.2i 475	. . . . . . 7 ⊢ (⟨1, 1⟩ ∈ V ∧ ⟨2, 2⟩ ∈ V)
37		opex 5435	. . . . . . . 8 ⊢ ⟨1, 2⟩ ∈ V
38		opex 5435	. . . . . . . 8 ⊢ ⟨2, 1⟩ ∈ V
39	37, 38	pm3.2i 475	. . . . . . 7 ⊢ (⟨1, 2⟩ ∈ V ∧ ⟨2, 1⟩ ∈ V)
40	36, 39	pm3.2i 475	. . . . . 6 ⊢ ((⟨1, 1⟩ ∈ V ∧ ⟨2, 2⟩ ∈ V) ∧ (⟨1, 2⟩ ∈ V ∧ ⟨2, 1⟩ ∈ V))
41		1ne2 12439	. . . . . . . . . 10 ⊢ 1 ≠ 2
42	41	olci 879	. . . . . . . . 9 ⊢ (1 ≠ 1 ∨ 1 ≠ 2)
43		1ex 11191	. . . . . . . . . 10 ⊢ 1 ∈ V
44	43, 43	opthne 5454	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ≠ ⟨1, 2⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 2))
45	42, 44	mpbir 234	. . . . . . . 8 ⊢ ⟨1, 1⟩ ≠ ⟨1, 2⟩
46	41	orci 878	. . . . . . . . 9 ⊢ (1 ≠ 2 ∨ 1 ≠ 1)
47	43, 43	opthne 5454	. . . . . . . . 9 ⊢ (⟨1, 1⟩ ≠ ⟨2, 1⟩ ↔ (1 ≠ 2 ∨ 1 ≠ 1))
48	46, 47	mpbir 234	. . . . . . . 8 ⊢ ⟨1, 1⟩ ≠ ⟨2, 1⟩
49	45, 48	pm3.2i 475	. . . . . . 7 ⊢ (⟨1, 1⟩ ≠ ⟨1, 2⟩ ∧ ⟨1, 1⟩ ≠ ⟨2, 1⟩)
50	49	orci 878	. . . . . 6 ⊢ ((⟨1, 1⟩ ≠ ⟨1, 2⟩ ∧ ⟨1, 1⟩ ≠ ⟨2, 1⟩) ∨ (⟨2, 2⟩ ≠ ⟨1, 2⟩ ∧ ⟨2, 2⟩ ≠ ⟨2, 1⟩))
51	40, 50	pm3.2i 475	. . . . 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 4814	. . . . 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 411	. . . 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 4674	. . . 4 ⊢ ({⟨1, 1⟩, ⟨2, 2⟩} ≠ {⟨1, 2⟩, ⟨2, 1⟩} → ({{⟨1, 1⟩, ⟨2, 2⟩}} ∩ {{⟨1, 2⟩, ⟨2, 1⟩}}) = ∅)
56	52, 54, 55	3syl 19	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ({{⟨1, 1⟩, ⟨2, 2⟩}} ∩ {{⟨1, 2⟩, ⟨2, 1⟩}}) = ∅)
57		2nn 12302	. . . . . 6 ⊢ 2 ∈ ℕ
58	18, 4, 15	symg2bas 19451	. . . . . 6 ⊢ ((1 ∈ V ∧ 2 ∈ ℕ) → (Base‘(SymGrp‘𝑁)) = {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}})
59	43, 57, 58	mp2an 704	. . . . 5 ⊢ (Base‘(SymGrp‘𝑁)) = {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
60		df-pr 4588	. . . . 5 ⊢ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}} = ({{⟨1, 1⟩, ⟨2, 2⟩}} ∪ {{⟨1, 2⟩, ⟨2, 1⟩}})
61	59, 60	eqtri 2788	. . . 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 19988	. 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 20313	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
65	64	adantr 485	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd)
66		prex 5399	. . . . . 6 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ V
67	66	a1i 11	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 1⟩, ⟨2, 2⟩} ∈ V)
68	66	prid1 4724	. . . . . . . . 9 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
69	68, 59	eleqtrri 2864	. . . . . . . 8 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁))
70	69	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁)))
71	4, 6, 5	zrhpsgnelbas 21701	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) ∈ (Base‘𝑅))
72	17, 71	mp3an2 1473	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) ∈ (Base‘𝑅))
73	70, 72	sylan2 604	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) ∈ (Base‘𝑅))
74	15, 4, 2, 3, 8	m2detleiblem2 22742	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
75	69, 74	mp3an2 1473	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
76	11, 7	ringcl 20320	. . . . . 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 1394	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
78		2fveq3 6876	. . . . . . 7 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})))
79		fveq1 6870	. . . . . . . . . 10 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑘‘𝑛) = ({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛))
80	79	oveq1d 7415	. . . . . . . . 9 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → ((𝑘‘𝑛)𝑀𝑛) = (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))
81	80	mpteq2dv 5198	. . . . . . . 8 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))
82	81	oveq2d 7416	. . . . . . 7 ⊢ (𝑘 = {⟨1, 1⟩, ⟨2, 2⟩} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))))
83	78, 82	oveq12d 7418	. . . . . 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 20012	. . . . 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 1394	. . . 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 5399	. . . . . 6 ⊢ {⟨1, 2⟩, ⟨2, 1⟩} ∈ V
87	86	a1i 11	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 2⟩, ⟨2, 1⟩} ∈ V)
88	86	prid2 4725	. . . . . . . . 9 ⊢ {⟨1, 2⟩, ⟨2, 1⟩} ∈ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
89	88, 59	eleqtrri 2864	. . . . . . . 8 ⊢ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁))
90	89	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁)))
91	4, 6, 5	zrhpsgnelbas 21701	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) ∈ (Base‘𝑅))
92	17, 91	mp3an2 1473	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) ∈ (Base‘𝑅))
93	90, 92	sylan2 604	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) ∈ (Base‘𝑅))
94	15, 4, 2, 3, 8	m2detleiblem2 22742	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
95	89, 94	mp3an2 1473	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
96	11, 7	ringcl 20320	. . . . . 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 1394	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
98		2fveq3 6876	. . . . . . 7 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})))
99		fveq1 6870	. . . . . . . . . 10 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → (𝑘‘𝑛) = ({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛))
100	99	oveq1d 7415	. . . . . . . . 9 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → ((𝑘‘𝑛)𝑀𝑛) = (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))
101	100	mpteq2dv 5198	. . . . . . . 8 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))
102	101	oveq2d 7416	. . . . . . 7 ⊢ (𝑘 = {⟨1, 2⟩, ⟨2, 1⟩} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))))
103	98, 102	oveq12d 7418	. . . . . 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 20012	. . . . 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 1394	. . . 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 7418	. . 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 2766	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩})
108		eqid 2765	. . . . . . . 8 ⊢ (1r‘𝑅) = (1r‘𝑅)
109	15, 4, 5, 6, 108	m2detleiblem5 22739	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩}) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) = (1r‘𝑅))
110	107, 109	sylan2 604	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) = (1r‘𝑅))
111		eqidd 2766	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 1⟩, ⟨2, 2⟩} = {⟨1, 1⟩, ⟨2, 2⟩})
112	8, 7	mgpplusg 20208	. . . . . . . 8 ⊢ · = (+g‘(mulGrp‘𝑅))
113	15, 4, 2, 3, 8, 112	m2detleiblem3 22743	. . . . . . 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 1394	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2)))
115	110, 114	oveq12d 7418	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))) = ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))))
116	43	prid1 4724	. . . . . . . . . 10 ⊢ 1 ∈ {1, 2}
117	116, 15	eleqtrri 2864	. . . . . . . . 9 ⊢ 1 ∈ 𝑁
118	117	a1i 11	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 1 ∈ 𝑁)
119	3	eleq2i 2857	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴))
120	119	bilani 509	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴))
121	2, 11	matecl 22539	. . . . . . . 8 ⊢ ((1 ∈ 𝑁 ∧ 1 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀1) ∈ (Base‘𝑅))
122	118, 118, 120, 121	syl3anc 1394	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀1) ∈ (Base‘𝑅))
123		prid2g 4723	. . . . . . . . . . 11 ⊢ (2 ∈ ℕ → 2 ∈ {1, 2})
124	57, 123	ax-mp 5	. . . . . . . . . 10 ⊢ 2 ∈ {1, 2}
125	124, 15	eleqtrri 2864	. . . . . . . . 9 ⊢ 2 ∈ 𝑁
126	125	a1i 11	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 2 ∈ 𝑁)
127	2, 11	matecl 22539	. . . . . . . 8 ⊢ ((2 ∈ 𝑁 ∧ 2 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀2) ∈ (Base‘𝑅))
128	126, 126, 120, 127	syl3anc 1394	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀2) ∈ (Base‘𝑅))
129	11, 7	ringcl 20320	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (1𝑀1) ∈ (Base‘𝑅) ∧ (2𝑀2) ∈ (Base‘𝑅)) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅))
130	22, 122, 128, 129	syl3anc 1394	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅))
131	11, 7, 108	ringlidm 20340	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2)))
132	130, 131	syldan 602	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2)))
133	115, 132	eqtrd 2800	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 1⟩, ⟨2, 2⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 1⟩, ⟨2, 2⟩}‘𝑛)𝑀𝑛)))) = ((1𝑀1) · (2𝑀2)))
134		eqidd 2766	. . . . . 6 ⊢ (𝑀 ∈ 𝐵 → {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩})
135		eqid 2765	. . . . . . 7 ⊢ (invg‘𝑅) = (invg‘𝑅)
136	15, 4, 5, 6, 108, 135	m2detleiblem6 22740	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩}) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) = ((invg‘𝑅)‘(1r‘𝑅)))
137	134, 136	sylan2 604	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) = ((invg‘𝑅)‘(1r‘𝑅)))
138		eqidd 2766	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩})
139	15, 4, 2, 3, 8, 112	m2detleiblem4 22744	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ {⟨1, 2⟩, ⟨2, 1⟩} = {⟨1, 2⟩, ⟨2, 1⟩} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2)))
140	22, 138, 28, 139	syl3anc 1394	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2)))
141	137, 140	oveq12d 7418	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨1, 2⟩, ⟨2, 1⟩})) · ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({⟨1, 2⟩, ⟨2, 1⟩}‘𝑛)𝑀𝑛)))) = (((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2))))
142	133, 141	oveq12d 7418	. . 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)))))
143	2, 11	matecl 22539	. . . . . 6 ⊢ ((2 ∈ 𝑁 ∧ 1 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀1) ∈ (Base‘𝑅))
144	126, 118, 120, 143	syl3anc 1394	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀1) ∈ (Base‘𝑅))
145	2, 11	matecl 22539	. . . . . 6 ⊢ ((1 ∈ 𝑁 ∧ 2 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀2) ∈ (Base‘𝑅))
146	118, 126, 120, 145	syl3anc 1394	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀2) ∈ (Base‘𝑅))
147	11, 7	ringcl 20320	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (2𝑀1) ∈ (Base‘𝑅) ∧ (1𝑀2) ∈ (Base‘𝑅)) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅))
148	22, 144, 146, 147	syl3anc 1394	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅))
149		m2detleib.m	. . . . 5 ⊢ − = (-g‘𝑅)
150	15, 4, 5, 6, 108, 135, 7, 149	m2detleiblem7 22741	. . . 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))))
151	22, 130, 148, 150	syl3anc 1394	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((1𝑀1) · (2𝑀2))(+g‘𝑅)(((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2))))
152	106, 142, 151	3eqtrd 2804	. 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))))
153	10, 63, 152	3eqtrd 2804	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2))))

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1563   ∈ wcel 2145   ≠ wne 2960  Vcvv 3457   ∪ cun 3905   ∩ cin 3906  ∅c0 4288  {csn 4585  {cpr 4587  ⟨cop 4591   ↦ cmpt 5185  ‘cfv 6525  (class class class)co 7400  Fincfn 8931  1c1 11089  ℕcn 12221  2c2 12283  Basecbs 17257  +_gcplusg 17298  ._rcmulr 17299   Σ_g cgsu 17481  Mndcmnd 18780  inv_gcminusg 18989  -_gcsg 18990  SymGrpcsymg 19427  pmSgncpsgn 19547  CMndccmn 19838  mulGrpcmgp 20204  1_rcur 20251  Ringcrg 20303  ℤRHomczrh 21606   Mat cmat 22521   maDet cmdat 22698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5231  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-addf 11167  ax-mulf 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-xor 1535  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-ot 4594  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7664  df-om 7851  df-1st 7974  df-2nd 7975  df-supp 8145  df-tpos 8210  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-oadd 8445  df-er 8682  df-map 8814  df-pm 8815  df-ixp 8884  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-fsupp 9310  df-sup 9390  df-oi 9460  df-dju 9875  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12222  df-2 12291  df-3 12292  df-4 12293  df-5 12294  df-6 12295  df-7 12296  df-8 12297  df-9 12298  df-n0 12493  df-xnn0 12566  df-z 12580  df-dec 12700  df-uz 12851  df-rp 13005  df-fz 13524  df-fzo 13671  df-seq 14026  df-exp 14086  df-fac 14298  df-bc 14327  df-hash 14355  df-word 14539  df-lsw 14588  df-concat 14596  df-s1 14622  df-substr 14667  df-pfx 14697  df-splice 14775  df-reverse 14784  df-s2 14873  df-struct 17195  df-sets 17212  df-slot 17230  df-ndx 17242  df-base 17258  df-ress 17279  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-0g 17482  df-gsum 17483  df-prds 17488  df-pws 17490  df-mre 17626  df-mrc 17627  df-acs 17629  df-mgm 18686  df-sgrp 18765  df-mnd 18781  df-mhm 18829  df-submnd 18830  df-efmnd 18916  df-grp 18991  df-minusg 18992  df-sbg 18993  df-mulg 19122  df-subg 19177  df-ghm 19272  df-gim 19317  df-cntz 19375  df-oppg 19404  df-symg 19428  df-pmtr 19500  df-psgn 19549  df-cmn 19840  df-abl 19841  df-mgp 20205  df-rng 20219  df-ur 20252  df-ring 20305  df-cring 20306  df-rhm 20542  df-subrng 20619  df-subrg 20643  df-sra 21260  df-rgmod 21261  df-cnfld 21480  df-zring 21554  df-zrh 21610  df-dsmm 21839  df-frlm 21854  df-mat 22522  df-mdet 22699

This theorem is referenced by:  lmat22det  34124