# 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. ) )`