# Metamath Proof Explorer

## 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 ‘ 𝑅 ) )