Metamath Proof Explorer

Theorem m2detleiblem1

Description: Lemma 1 for m2detleib . (Contributed by AV, 12-Dec-2018)

Ref Expression
Hypotheses m2detleiblem1.n 
|- N = { 1 , 2 }
m2detleiblem1.p 
|- P = ( Base ` ( SymGrp ` N ) )
m2detleiblem1.y 
|- Y = ( ZRHom ` R )
m2detleiblem1.s 
|- S = ( pmSgn ` N )
m2detleiblem1.o 
|- .1. = ( 1r ` R )
Assertion m2detleiblem1 
|- ( ( R e. Ring /\ Q e. P ) -> ( Y ` ( S ` Q ) ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )

Proof

Step Hyp Ref Expression
1 m2detleiblem1.n 
 |-  N = { 1 , 2 }
2 m2detleiblem1.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
3 m2detleiblem1.y 
 |-  Y = ( ZRHom ` R )
4 m2detleiblem1.s 
 |-  S = ( pmSgn ` N )
5 m2detleiblem1.o 
 |-  .1. = ( 1r ` R )
6 elpri 
 |-  ( Q e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } -> ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } \/ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
7 fveq2 
 |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( S ` Q ) = ( S ` { <. 1 , 1 >. , <. 2 , 2 >. } ) )
8 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
9 eqid 
 |-  ran ( pmTrsp ` N ) = ran ( pmTrsp ` N )
10 1 8 2 9 4 psgnprfval1 
 |-  ( S ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = 1
11 7 10 eqtrdi 
 |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( S ` Q ) = 1 )
12 1z 
 |-  1 e. ZZ
13 11 12 eqeltrdi 
 |-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( S ` Q ) e. ZZ )
14 fveq2 
 |-  ( Q = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( S ` Q ) = ( S ` { <. 1 , 2 >. , <. 2 , 1 >. } ) )
15 1 8 2 9 4 psgnprfval2 
 |-  ( S ` { <. 1 , 2 >. , <. 2 , 1 >. } ) = -u 1
16 14 15 eqtrdi 
 |-  ( Q = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( S ` Q ) = -u 1 )
17 neg1z 
 |-  -u 1 e. ZZ
18 16 17 eqeltrdi 
 |-  ( Q = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( S ` Q ) e. ZZ )
19 13 18 jaoi 
 |-  ( ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } \/ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( S ` Q ) e. ZZ )
20 6 19 syl 
 |-  ( Q e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } -> ( S ` Q ) e. ZZ )
21 1ex 
 |-  1 e. _V
22 2nn 
 |-  2 e. NN
23 8 2 1 symg2bas 
 |-  ( ( 1 e. _V /\ 2 e. NN ) -> P = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )
24 21 22 23 mp2an 
 |-  P = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }
25 20 24 eleq2s 
 |-  ( Q e. P -> ( S ` Q ) e. ZZ )
26 eqid 
 |-  ( .g ` R ) = ( .g ` R )
27 3 26 5 zrhmulg 
 |-  ( ( R e. Ring /\ ( S ` Q ) e. ZZ ) -> ( Y ` ( S ` Q ) ) = ( ( S ` Q ) ( .g ` R ) .1. ) )
28 25 27 sylan2 
 |-  ( ( R e. Ring /\ Q e. P ) -> ( Y ` ( S ` Q ) ) = ( ( S ` Q ) ( .g ` R ) .1. ) )
29 4 a1i 
 |-  ( ( R e. Ring /\ Q e. P ) -> S = ( pmSgn ` N ) )
30 29 fveq1d 
 |-  ( ( R e. Ring /\ Q e. P ) -> ( S ` Q ) = ( ( pmSgn ` N ) ` Q ) )
31 30 oveq1d 
 |-  ( ( R e. Ring /\ Q e. P ) -> ( ( S ` Q ) ( .g ` R ) .1. ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )
32 28 31 eqtrd 
 |-  ( ( R e. Ring /\ Q e. P ) -> ( Y ` ( S ` Q ) ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )