m2detleiblem4

Description: Lemma 4 for m2detleib . (Contributed by AV, 20-Dec-2018) (Proof shortened by AV, 2-Jan-2019)

	Ref	Expression
Hypotheses	m2detleiblem2.n	$⊢ N = \{1, 2\}$
	m2detleiblem2.p	$⊢ P = {Base}_{SymGrp (N)}$
	m2detleiblem2.a	$⊢ A = N Mat R$
	m2detleiblem2.b	$⊢ B = {Base}_{A}$
	m2detleiblem2.g	$⊢ G = {mulGrp}_{R}$
	m2detleiblem3.m	$⊢ \underset{˙}{\cdot} = +_{G}$
Assertion	m2detleiblem4	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to \underset{n \in N}{\sum_{G}} (Q (n) M n) = (2 M 1) \underset{˙}{\cdot} (1 M 2)$

Proof

Step	Hyp	Ref	Expression
1		m2detleiblem2.n	$⊢ N = \{1, 2\}$
2		m2detleiblem2.p	$⊢ P = {Base}_{SymGrp (N)}$
3		m2detleiblem2.a	$⊢ A = N Mat R$
4		m2detleiblem2.b	$⊢ B = {Base}_{A}$
5		m2detleiblem2.g	$⊢ G = {mulGrp}_{R}$
6		m2detleiblem3.m	$⊢ \underset{˙}{\cdot} = +_{G}$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	5 7	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
9	5	fvexi	$⊢ G \in V$
10	9	a1i	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to G \in V$
11		1ex	$⊢ 1 \in V$
12		2nn	$⊢ 2 \in ℕ$
13		prex	$⊢ \{⟨1, 2⟩, ⟨2, 1⟩\} \in V$
14	13	prid2	$⊢ \{⟨1, 2⟩, ⟨2, 1⟩\} \in \{\{⟨1, 1⟩, ⟨2, 2⟩\}, \{⟨1, 2⟩, ⟨2, 1⟩\}\}$
15		eqid	$⊢ SymGrp (N) = SymGrp (N)$
16	15 2 1	symg2bas	$⊢ (1 \in V \land 2 \in ℕ) \to P = \{\{⟨1, 1⟩, ⟨2, 2⟩\}, \{⟨1, 2⟩, ⟨2, 1⟩\}\}$
17	14 16	eleqtrrid	$⊢ (1 \in V \land 2 \in ℕ) \to \{⟨1, 2⟩, ⟨2, 1⟩\} \in P$
18	11 12 17	mp2an	$⊢ \{⟨1, 2⟩, ⟨2, 1⟩\} \in P$
19		eleq1	$⊢ Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \to (Q \in P \leftrightarrow \{⟨1, 2⟩, ⟨2, 1⟩\} \in P)$
20	18 19	mpbiri	$⊢ Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \to Q \in P$
21	1	oveq1i	$⊢ N Mat R = \{1, 2\} Mat R$
22	3 21	eqtri	$⊢ A = \{1, 2\} Mat R$
23	1	fveq2i	$⊢ SymGrp (N) = SymGrp (\{1, 2\})$
24	23	fveq2i	$⊢ {Base}_{SymGrp (N)} = {Base}_{SymGrp (\{1, 2\})}$
25	2 24	eqtri	$⊢ P = {Base}_{SymGrp (\{1, 2\})}$
26	22 4 25	matepmcl	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \forall n \in \{1, 2\} Q (n) M n \in {Base}_{R}$
27	20 26	syl3an2	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to \forall n \in \{1, 2\} Q (n) M n \in {Base}_{R}$
28	1	mpteq1i	$⊢ (n \in N ⟼ Q (n) M n) = (n \in \{1, 2\} ⟼ Q (n) M n)$
29	28	fmpt	$⊢ \forall n \in \{1, 2\} Q (n) M n \in {Base}_{R} \leftrightarrow (n \in N ⟼ Q (n) M n) : \{1, 2\} ⟶ {Base}_{R}$
30	27 29	sylib	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to (n \in N ⟼ Q (n) M n) : \{1, 2\} ⟶ {Base}_{R}$
31	8 6 10 30	gsumpr12val	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to \underset{n \in N}{\sum_{G}} (Q (n) M n) = (n \in N ⟼ Q (n) M n) (1) \underset{˙}{\cdot} (n \in N ⟼ Q (n) M n) (2)$
32	11	prid1	$⊢ 1 \in \{1, 2\}$
33	32 1	eleqtrri	$⊢ 1 \in N$
34	3 4 2	matepmcl	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \forall n \in N Q (n) M n \in {Base}_{R}$
35	20 34	syl3an2	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to \forall n \in N Q (n) M n \in {Base}_{R}$
36		fveq2	$⊢ n = 1 \to Q (n) = Q (1)$
37		id	$⊢ n = 1 \to n = 1$
38	36 37	oveq12d	$⊢ n = 1 \to Q (n) M n = Q (1) M 1$
39	38	eleq1d	$⊢ n = 1 \to (Q (n) M n \in {Base}_{R} \leftrightarrow Q (1) M 1 \in {Base}_{R})$
40	39	rspcva	$⊢ (1 \in N \land \forall n \in N Q (n) M n \in {Base}_{R}) \to Q (1) M 1 \in {Base}_{R}$
41	33 35 40	sylancr	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to Q (1) M 1 \in {Base}_{R}$
42		eqid	$⊢ (n \in N ⟼ Q (n) M n) = (n \in N ⟼ Q (n) M n)$
43	38 42	fvmptg	$⊢ (1 \in N \land Q (1) M 1 \in {Base}_{R}) \to (n \in N ⟼ Q (n) M n) (1) = Q (1) M 1$
44	33 41 43	sylancr	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to (n \in N ⟼ Q (n) M n) (1) = Q (1) M 1$
45		fveq1	$⊢ Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \to Q (1) = \{⟨1, 2⟩, ⟨2, 1⟩\} (1)$
46		1ne2	$⊢ 1 \neq 2$
47		2ex	$⊢ 2 \in V$
48	11 47	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, 2⟩, ⟨2, 1⟩\} (1) = 2$
49	46 48	ax-mp	$⊢ \{⟨1, 2⟩, ⟨2, 1⟩\} (1) = 2$
50	45 49	eqtrdi	$⊢ Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \to Q (1) = 2$
51	50	3ad2ant2	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to Q (1) = 2$
52	51	oveq1d	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to Q (1) M 1 = 2 M 1$
53	44 52	eqtrd	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to (n \in N ⟼ Q (n) M n) (1) = 2 M 1$
54	47	prid2	$⊢ 2 \in \{1, 2\}$
55	54 1	eleqtrri	$⊢ 2 \in N$
56		fveq2	$⊢ n = 2 \to Q (n) = Q (2)$
57		id	$⊢ n = 2 \to n = 2$
58	56 57	oveq12d	$⊢ n = 2 \to Q (n) M n = Q (2) M 2$
59	58	eleq1d	$⊢ n = 2 \to (Q (n) M n \in {Base}_{R} \leftrightarrow Q (2) M 2 \in {Base}_{R})$
60	59	rspcva	$⊢ (2 \in N \land \forall n \in N Q (n) M n \in {Base}_{R}) \to Q (2) M 2 \in {Base}_{R}$
61	55 35 60	sylancr	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to Q (2) M 2 \in {Base}_{R}$
62	58 42	fvmptg	$⊢ (2 \in N \land Q (2) M 2 \in {Base}_{R}) \to (n \in N ⟼ Q (n) M n) (2) = Q (2) M 2$
63	55 61 62	sylancr	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to (n \in N ⟼ Q (n) M n) (2) = Q (2) M 2$
64		fveq1	$⊢ Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \to Q (2) = \{⟨1, 2⟩, ⟨2, 1⟩\} (2)$
65	47 11	fvpr2	$⊢ 1 \neq 2 \to \{⟨1, 2⟩, ⟨2, 1⟩\} (2) = 1$
66	46 65	ax-mp	$⊢ \{⟨1, 2⟩, ⟨2, 1⟩\} (2) = 1$
67	64 66	eqtrdi	$⊢ Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \to Q (2) = 1$
68	67	3ad2ant2	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to Q (2) = 1$
69	68	oveq1d	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to Q (2) M 2 = 1 M 2$
70	63 69	eqtrd	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to (n \in N ⟼ Q (n) M n) (2) = 1 M 2$
71	53 70	oveq12d	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to (n \in N ⟼ Q (n) M n) (1) \underset{˙}{\cdot} (n \in N ⟼ Q (n) M n) (2) = (2 M 1) \underset{˙}{\cdot} (1 M 2)$
72	31 71	eqtrd	$⊢ (R \in Ring \land Q = \{⟨1, 2⟩, ⟨2, 1⟩\} \land M \in B) \to \underset{n \in N}{\sum_{G}} (Q (n) M n) = (2 M 1) \underset{˙}{\cdot} (1 M 2)$

Metamath Proof Explorer

Theorem m2detleiblem4

Proof