Theorem m2detleiblem4

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

	Ref	Expression
Hypotheses	m2detleiblem2.n	⊢ 𝑁 = { 1 , 2 }
	m2detleiblem2.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	m2detleiblem2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	m2detleiblem2.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	m2detleiblem2.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	m2detleiblem3.m	⊢ · = ( +g ‘ 𝐺 )
Assertion	m2detleiblem4	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		m2detleiblem2.n	⊢ 𝑁 = { 1 , 2 }
2		m2detleiblem2.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
3		m2detleiblem2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		m2detleiblem2.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
5		m2detleiblem2.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
6		m2detleiblem3.m	⊢ · = ( +g ‘ 𝐺 )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8	5 7	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
9	5	fvexi	⊢ 𝐺 ∈ V
10	9	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ V )
11		1ex	⊢ 1 ∈ V
12		2nn	⊢ 2 ∈ ℕ
13		prex	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
14	13	prid2	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
15		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
16	15 2 1	symg2bas	⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝑃 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
17	14 16	eleqtrrid	⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 )
18	11 12 17	mp2an	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃
19		eleq1	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ∈ 𝑃 ↔ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 ) )
20	18 19	mpbiri	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → 𝑄 ∈ 𝑃 )
21	1	oveq1i	⊢ ( 𝑁 Mat 𝑅 ) = ( { 1 , 2 } Mat 𝑅 )
22	3 21	eqtri	⊢ 𝐴 = ( { 1 , 2 } Mat 𝑅 )
23	1	fveq2i	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ { 1 , 2 } )
24	23	fveq2i	⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ { 1 , 2 } ) )
25	2 24	eqtri	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ { 1 , 2 } ) )
26	22 4 25	matepmcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ { 1 , 2 } ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
27	20 26	syl3an2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ { 1 , 2 } ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
28	1	mpteq1i	⊢ ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛 ∈ { 1 , 2 } ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) )
29	28	fmpt	⊢ ( ∀ 𝑛 ∈ { 1 , 2 } ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ↔ ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) : { 1 , 2 } ⟶ ( Base ‘ 𝑅 ) )
30	27 29	sylib	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) : { 1 , 2 } ⟶ ( Base ‘ 𝑅 ) )
31	8 6 10 30	gsumpr12val	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) · ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) ) )
32	11	prid1	⊢ 1 ∈ { 1 , 2 }
33	32 1	eleqtrri	⊢ 1 ∈ 𝑁
34	3 4 2	matepmcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
35	20 34	syl3an2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
36		fveq2	⊢ ( 𝑛 = 1 → ( 𝑄 ‘ 𝑛 ) = ( 𝑄 ‘ 1 ) )
37		id	⊢ ( 𝑛 = 1 → 𝑛 = 1 )
38	36 37	oveq12d	⊢ ( 𝑛 = 1 → ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) = ( ( 𝑄 ‘ 1 ) 𝑀 1 ) )
39	38	eleq1d	⊢ ( 𝑛 = 1 → ( ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ) )
40	39	rspcva	⊢ ( ( 1 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
41	33 35 40	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) )
42		eqid	⊢ ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) = ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) )
43	38 42	fvmptg	⊢ ( ( 1 ∈ 𝑁 ∧ ( ( 𝑄 ‘ 1 ) 𝑀 1 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) = ( ( 𝑄 ‘ 1 ) 𝑀 1 ) )
44	33 41 43	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) = ( ( 𝑄 ‘ 1 ) 𝑀 1 ) )
45		fveq1	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 1 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) )
46		1ne2	⊢ 1 ≠ 2
47		2ex	⊢ 2 ∈ V
48	11 47	fvpr1	⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 2 )
49	46 48	ax-mp	⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 2
50	45 49	eqtrdi	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 1 ) = 2 )
51	50	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 ‘ 1 ) = 2 )
52	51	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 1 ) 𝑀 1 ) = ( 2 𝑀 1 ) )
53	44 52	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) = ( 2 𝑀 1 ) )
54	47	prid2	⊢ 2 ∈ { 1 , 2 }
55	54 1	eleqtrri	⊢ 2 ∈ 𝑁
56		fveq2	⊢ ( 𝑛 = 2 → ( 𝑄 ‘ 𝑛 ) = ( 𝑄 ‘ 2 ) )
57		id	⊢ ( 𝑛 = 2 → 𝑛 = 2 )
58	56 57	oveq12d	⊢ ( 𝑛 = 2 → ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) = ( ( 𝑄 ‘ 2 ) 𝑀 2 ) )
59	58	eleq1d	⊢ ( 𝑛 = 2 → ( ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) )
60	59	rspcva	⊢ ( ( 2 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
61	55 35 60	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) )
62	58 42	fvmptg	⊢ ( ( 2 ∈ 𝑁 ∧ ( ( 𝑄 ‘ 2 ) 𝑀 2 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) = ( ( 𝑄 ‘ 2 ) 𝑀 2 ) )
63	55 61 62	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) = ( ( 𝑄 ‘ 2 ) 𝑀 2 ) )
64		fveq1	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 2 ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) )
65	47 11	fvpr2	⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1 )
66	46 65	ax-mp	⊢ ( { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1
67	64 66	eqtrdi	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ‘ 2 ) = 1 )
68	67	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝑄 ‘ 2 ) = 1 )
69	68	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑄 ‘ 2 ) 𝑀 2 ) = ( 1 𝑀 2 ) )
70	63 69	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) = ( 1 𝑀 2 ) )
71	53 70	oveq12d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 1 ) · ( ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ‘ 2 ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )
72	31 71	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) = ( ( 2 𝑀 1 ) · ( 1 𝑀 2 ) ) )