Theorem m2detleiblem2

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

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

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		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	5 6	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
8	5	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Mnd )
9	8	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
10		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
11	10	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → 2 ∈ ( ℤ≥ ‘ 1 ) )
12		1z	⊢ 1 ∈ ℤ
13		fzpr	⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
14	12 13	ax-mp	⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
15		1p1e2	⊢ ( 1 + 1 ) = 2
16	15	preq2i	⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 }
17	14 16	eqtri	⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , 2 }
18		df-2	⊢ 2 = ( 1 + 1 )
19	18	oveq2i	⊢ ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
20	17 19 1	3eqtr4ri	⊢ 𝑁 = ( 1 ... 2 )
21	20	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → 𝑁 = ( 1 ... 2 ) )
22	3 4 2	matepmcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
23	7 9 11 21 22	gsummptfzcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( ( 𝑄 ‘ 𝑛 ) 𝑀 𝑛 ) ) ) ∈ ( Base ‘ 𝑅 ) )