Metamath Proof Explorer

Theorem m2detleiblem6

Description: Lemma 6 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 )
m2detleiblem1.i 
|- I = ( invg ` R )
Assertion m2detleiblem6 
|- ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( Y ` ( S ` Q ) ) = ( I ` .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 m2detleiblem1.i 
 |-  I = ( invg ` R )
7 1ex 
 |-  1 e. _V
8 2nn 
 |-  2 e. NN
9 prex 
 |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. _V
10 9 prid2 
 |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } }
11 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
12 11 2 1 symg2bas 
 |-  ( ( 1 e. _V /\ 2 e. NN ) -> P = { { <. 1 , 1 >. , <. 2 , 2 >. } , { <. 1 , 2 >. , <. 2 , 1 >. } } )
13 10 12 eleqtrrid 
 |-  ( ( 1 e. _V /\ 2 e. NN ) -> { <. 1 , 2 >. , <. 2 , 1 >. } e. P )
14 7 8 13 mp2an 
 |-  { <. 1 , 2 >. , <. 2 , 1 >. } e. P
15 eleq1 
 |-  ( Q = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( Q e. P <-> { <. 1 , 2 >. , <. 2 , 1 >. } e. P ) )
16 14 15 mpbiri 
 |-  ( Q = { <. 1 , 2 >. , <. 2 , 1 >. } -> Q e. P )
17 1 2 3 4 5 m2detleiblem1 
 |-  ( ( R e. Ring /\ Q e. P ) -> ( Y ` ( S ` Q ) ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )
18 16 17 sylan2 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( Y ` ( S ` Q ) ) = ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) )
19 fveq2 
 |-  ( Q = { <. 1 , 2 >. , <. 2 , 1 >. } -> ( ( pmSgn ` N ) ` Q ) = ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) )
20 19 adantl 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( ( pmSgn ` N ) ` Q ) = ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) )
21 eqid 
 |-  ran ( pmTrsp ` N ) = ran ( pmTrsp ` N )
22 eqid 
 |-  ( pmSgn ` N ) = ( pmSgn ` N )
23 1 11 2 21 22 psgnprfval2 
 |-  ( ( pmSgn ` N ) ` { <. 1 , 2 >. , <. 2 , 1 >. } ) = -u 1
24 20 23 eqtrdi 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( ( pmSgn ` N ) ` Q ) = -u 1 )
25 24 oveq1d 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( ( ( pmSgn ` N ) ` Q ) ( .g ` R ) .1. ) = ( -u 1 ( .g ` R ) .1. ) )
26 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
27 eqid 
 |-  ( Base ` R ) = ( Base ` R )
28 27 5 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
29 eqid 
 |-  ( .g ` R ) = ( .g ` R )
30 27 29 6 mulgm1 
 |-  ( ( R e. Grp /\ .1. e. ( Base ` R ) ) -> ( -u 1 ( .g ` R ) .1. ) = ( I ` .1. ) )
31 26 28 30 syl2anc 
 |-  ( R e. Ring -> ( -u 1 ( .g ` R ) .1. ) = ( I ` .1. ) )
32 31 adantr 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( -u 1 ( .g ` R ) .1. ) = ( I ` .1. ) )
33 18 25 32 3eqtrd 
 |-  ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( Y ` ( S ` Q ) ) = ( I ` .1. ) )