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 >. } ) )
19 18 adantl 
 |-  ( ( 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 ) )
27 26 adantr 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> .1. e. ( Base ` R ) )
28 eqid 
 |-  ( .g ` R ) = ( .g ` R )
29 25 28 mulg1 
 |-  ( .1. e. ( Base ` R ) -> ( 1 ( .g ` R ) .1. ) = .1. )
30 27 29 syl 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( 1 ( .g ` R ) .1. ) = .1. )
31 17 24 30 3eqtrd 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( Y ` ( S ` Q ) ) = .1. )