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	$⊢ N = \{1, 2\}$
	m2detleib.d	$⊢ D = N maDet R$
	m2detleib.a	$⊢ A = N Mat R$
	m2detleib.b	$⊢ B = {Base}_{A}$
	m2detleib.m	$⊢ \underset{˙}{-} = -_{R}$
	m2detleib.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	m2detleib	$⊢ (R \in Ring \land M \in B) \to D (M) = ((1 M 1) \underset{˙}{\cdot} (2 M 2)) \underset{˙}{-} ((2 M 1) \underset{˙}{\cdot} (1 M 2))$

Proof

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

Metamath Proof Explorer

Theorem m2detleib

Proof