# 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
`|- 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 )`
Assertion m2detleiblem2
`|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) e. ( Base ` R ) )`

### 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 eqid
` |-  ( Base ` R ) = ( Base ` R )`
7 5 6 mgpbas
` |-  ( Base ` R ) = ( Base ` G )`
8 5 ringmgp
` |-  ( R e. Ring -> G e. Mnd )`
` |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> G e. Mnd )`
10 2eluzge1
` |-  2 e. ( ZZ>= ` 1 )`
11 10 a1i
` |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> 2 e. ( ZZ>= ` 1 ) )`
12 1z
` |-  1 e. ZZ`
13 fzpr
` |-  ( 1 e. ZZ -> ( 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
` |-  N = ( 1 ... 2 )`
21 20 a1i
` |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> N = ( 1 ... 2 ) )`
22 3 4 2 matepmcl
` |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) )`
23 7 9 11 21 22 gsummptfzcl
` |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) e. ( Base ` R ) )`