# Metamath Proof Explorer

## Theorem m2detleiblem5

Description: Lemma 5 for m2detleib . (Contributed by AV, 20-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 m2detleiblem5
|- ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( Y ` ( S ` Q ) ) = .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 1ex
|-  1 e. _V
7 2nn
|-  2 e. NN
8 prex
|-  { <. 1 , 1 >. , <. 2 , 2 >. } e. _V
9 8 prid1
|-  { <. 1 , 1 >. , <. 2 , 2 >. } e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }
10 eqid
|-  ( SymGrp ` N ) = ( SymGrp ` N )
11 10 2 1 symg2bas
|-  ( ( 1 e. _V /\ 2 e. NN ) -> P = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )
12 9 11 eleqtrrid
|-  ( ( 1 e. _V /\ 2 e. NN ) -> { <. 1 , 1 >. , <. 2 , 2 >. } e. P )
13 6 7 12 mp2an
|-  { <. 1 , 1 >. , <. 2 , 2 >. } e. P
14 eleq1
|-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( Q e. P <-> { <. 1 , 1 >. , <. 2 , 2 >. } e. P ) )
15 13 14 mpbiri
|-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> Q e. P )
16 1 2 3 4 5 m2detleiblem1
|-  ( ( R e. Ring /\ Q e. P ) -> ( Y ` ( S ` Q ) ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )
17 15 16 sylan2
|-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( Y ` ( S ` Q ) ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )
18 fveq2
|-  ( Q = { <. 1 , 1 >. , <. 2 , 2 >. } -> ( ( pmSgn ` N ) ` Q ) = ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) )
|-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( ( pmSgn ` N ) ` Q ) = ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) )
20 eqid
|-  ran ( pmTrsp ` N ) = ran ( pmTrsp ` N )
21 eqid
|-  ( pmSgn ` N ) = ( pmSgn ` N )
22 1 10 2 20 21 psgnprfval1
|-  ( ( pmSgn ` N ) ` { <. 1 , 1 >. , <. 2 , 2 >. } ) = 1
23 19 22 eqtrdi
|-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( ( pmSgn ` N ) ` Q ) = 1 )
24 23 oveq1d
|-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) = ( 1 ( .g ` R ) .1. ) )
25 eqid
|-  ( Base ` R ) = ( Base ` R )
26 25 5 ringidcl
|-  ( R e. Ring -> .1. e. ( Base ` R ) )