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 )
50 49 3ad2ant2 
 |-  ( ( 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 )
68 67 3ad2ant2 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( Q ` 2 ) = 2 )
69 68 oveq1d 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( Q ` 2 ) M 2 ) = ( 2 M 2 ) )
70 63 69 eqtrd 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( ( n e. N |-> ( ( Q ` n ) M n ) ) ` 2 ) = ( 2 M 2 ) )
71 52 70 oveq12d 
 |-  ( ( 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 ) ) )
72 31 71 eqtrd 
 |-  ( ( 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 ) ) )