# Metamath Proof Explorer

## Theorem m2detleiblem3

Description: Lemma 3 for m2detleib . (Contributed by AV, 16-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
`|- .x. = ( +g ` G )`
Assertion m2detleiblem3
`|- ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) = ( ( 1 M 1 ) .x. ( 2 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
` |-  .x. = ( +g ` G )`
7 eqid
` |-  ( Base ` R ) = ( Base ` R )`
8 5 7 mgpbas
` |-  ( Base ` R ) = ( Base ` G )`
9 5 fvexi
` |-  G e. _V`
10 9 a1i
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> G e. _V )`
11 1ex
` |-  1 e. _V`
12 2nn
` |-  2 e. NN`
13 prex
` |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. _V`
14 13 prid1
` |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }`
15 eqid
` |-  ( SymGrp ` N ) = ( SymGrp ` N )`
16 15 2 1 symg2bas
` |-  ( ( 1 e. _V /\ 2 e. NN ) -> P = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )`
17 14 16 eleqtrrid
` |-  ( ( 1 e. _V /\ 2 e. NN ) -> { <. 1 , 1 >. , <. 2 , 2 >. } e. P )`
18 11 12 17 mp2an
` |-  { <. 1 , 1 >. , <. 2 , 2 >. } e. P`
19 eleq1
` |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( Q e. P <-> { <. 1 , 1 >. , <. 2 , 2 >. } e. P ) )`
20 18 19 mpbiri
` |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> Q e. 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 e. Ring /\ Q e. P /\ M e. B ) -> A. n e. { 1 , 2 } ( ( Q ` n ) M n ) e. ( Base ` R ) )`
27 20 26 syl3an2
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> A. n e. { 1 , 2 } ( ( Q ` n ) M n ) e. ( Base ` R ) )`
28 1 mpteq1i
` |-  ( n e. N |-> ( ( Q ` n ) M n ) ) = ( n e. { 1 , 2 } |-> ( ( Q ` n ) M n ) )`
29 28 fmpt
` |-  ( A. n e. { 1 , 2 } ( ( Q ` n ) M n ) e. ( Base ` R ) <-> ( n e. N |-> ( ( Q ` n ) M n ) ) : { 1 , 2 } --> ( Base ` R ) )`
30 27 29 sylib
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( n e. N |-> ( ( Q ` n ) M n ) ) : { 1 , 2 } --> ( Base ` R ) )`
31 8 6 10 30 gsumpr12val
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) = ( ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 1 ) .x. ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 2 ) ) )`
32 11 prid1
` |-  1 e. { 1 , 2 }`
33 32 1 eleqtrri
` |-  1 e. N`
34 3 4 2 matepmcl
` |-  ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) )`
35 20 34 syl3an2
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) )`
36 fveq2
` |-  ( n = 1 -> ( Q ` n ) = ( Q ` 1 ) )`
37 id
` |-  ( n = 1 -> n = 1 )`
38 36 37 oveq12d
` |-  ( n = 1 -> ( ( Q ` n ) M n ) = ( ( Q ` 1 ) M 1 ) )`
39 38 eleq1d
` |-  ( n = 1 -> ( ( ( Q ` n ) M n ) e. ( Base ` R ) <-> ( ( Q ` 1 ) M 1 ) e. ( Base ` R ) ) )`
40 39 rspcva
` |-  ( ( 1 e. N /\ A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) ) -> ( ( Q ` 1 ) M 1 ) e. ( Base ` R ) )`
41 33 35 40 sylancr
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( Q ` 1 ) M 1 ) e. ( Base ` R ) )`
42 eqid
` |-  ( n e. N |-> ( ( Q ` n ) M n ) ) = ( n e. N |-> ( ( Q ` n ) M n ) )`
43 38 42 fvmptg
` |-  ( ( 1 e. N /\ ( ( Q ` 1 ) M 1 ) e. ( Base ` R ) ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 1 ) = ( ( Q ` 1 ) M 1 ) )`
44 33 41 43 sylancr
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 1 ) = ( ( Q ` 1 ) M 1 ) )`
45 fveq1
` |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( Q ` 1 ) = ( { <. 1 , 1 >. , <. 2 , 2 >. } ` 1 ) )`
46 1ne2
` |-  1 =/= 2`
47 11 11 fvpr1
` |-  ( 1 =/= 2 -> ( { <. 1 , 1 >. , <. 2 , 2 >. } ` 1 ) = 1 )`
48 46 47 ax-mp
` |-  ( { <. 1 , 1 >. , <. 2 , 2 >. } ` 1 ) = 1`
49 45 48 eqtrdi
` |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( Q ` 1 ) = 1 )`
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( Q ` 1 ) = 1 )`
51 50 oveq1d
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( Q ` 1 ) M 1 ) = ( 1 M 1 ) )`
52 44 51 eqtrd
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 1 ) = ( 1 M 1 ) )`
53 2ex
` |-  2 e. _V`
54 53 prid2
` |-  2 e. { 1 , 2 }`
55 54 1 eleqtrri
` |-  2 e. N`
56 fveq2
` |-  ( n = 2 -> ( Q ` n ) = ( Q ` 2 ) )`
57 id
` |-  ( n = 2 -> n = 2 )`
58 56 57 oveq12d
` |-  ( n = 2 -> ( ( Q ` n ) M n ) = ( ( Q ` 2 ) M 2 ) )`
59 58 eleq1d
` |-  ( n = 2 -> ( ( ( Q ` n ) M n ) e. ( Base ` R ) <-> ( ( Q ` 2 ) M 2 ) e. ( Base ` R ) ) )`
60 59 rspcva
` |-  ( ( 2 e. N /\ A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) ) -> ( ( Q ` 2 ) M 2 ) e. ( Base ` R ) )`
61 55 35 60 sylancr
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( Q ` 2 ) M 2 ) e. ( Base ` R ) )`
62 58 42 fvmptg
` |-  ( ( 2 e. N /\ ( ( Q ` 2 ) M 2 ) e. ( Base ` R ) ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 2 ) = ( ( Q ` 2 ) M 2 ) )`
63 55 61 62 sylancr
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 2 ) = ( ( Q ` 2 ) M 2 ) )`
64 fveq1
` |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( Q ` 2 ) = ( { <. 1 , 1 >. , <. 2 , 2 >. } ` 2 ) )`
65 53 53 fvpr2
` |-  ( 1 =/= 2 -> ( { <. 1 , 1 >. , <. 2 , 2 >. } ` 2 ) = 2 )`
66 46 65 ax-mp
` |-  ( { <. 1 , 1 >. , <. 2 , 2 >. } ` 2 ) = 2`
67 64 66 eqtrdi
` |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( Q ` 2 ) = 2 )`
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( Q ` 2 ) = 2 )`
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( Q ` 2 ) M 2 ) = ( 2 M 2 ) )`
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 2 ) = ( 2 M 2 ) )`
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 1 ) .x. ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 2 ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`
` |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )`