Metamath Proof Explorer

Theorem zrhpsgnelbas

Description: Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019)

Ref Expression
Hypotheses zrhpsgnelbas.p 
|- P = ( Base ` ( SymGrp ` N ) )
zrhpsgnelbas.s 
|- S = ( pmSgn ` N )
zrhpsgnelbas.y 
|- Y = ( ZRHom ` R )
Assertion zrhpsgnelbas 
|- ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) )

Proof

Step Hyp Ref Expression
1 zrhpsgnelbas.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 zrhpsgnelbas.s 
 |-  S = ( pmSgn ` N )
3 zrhpsgnelbas.y 
 |-  Y = ( ZRHom ` R )
4 1 2 psgnran 
 |-  ( ( N e. Fin /\ Q e. P ) -> ( S ` Q ) e. { 1 , -u 1 } )
5 4 3adant1 
 |-  ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( S ` Q ) e. { 1 , -u 1 } )
6 elpri 
 |-  ( ( S ` Q ) e. { 1 , -u 1 } -> ( ( S ` Q ) = 1 \/ ( S ` Q ) = -u 1 ) )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 3 7 zrh1 
 |-  ( R e. Ring -> ( Y ` 1 ) = ( 1r ` R ) )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 9 7 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
11 8 10 eqeltrd 
 |-  ( R e. Ring -> ( Y ` 1 ) e. ( Base ` R ) )
12 11 3ad2ant1 
 |-  ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` 1 ) e. ( Base ` R ) )
13 fveq2 
 |-  ( ( S ` Q ) = 1 -> ( Y ` ( S ` Q ) ) = ( Y ` 1 ) )
14 13 eleq1d 
 |-  ( ( S ` Q ) = 1 -> ( ( Y ` ( S ` Q ) ) e. ( Base ` R ) <-> ( Y ` 1 ) e. ( Base ` R ) ) )
15 12 14 imbitrrid 
 |-  ( ( S ` Q ) = 1 -> ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) ) )
16 neg1z 
 |-  -u 1 e. ZZ
17 eqid 
 |-  ( .g ` R ) = ( .g ` R )
18 3 17 7 zrhmulg 
 |-  ( ( R e. Ring /\ -u 1 e. ZZ ) -> ( Y ` -u 1 ) = ( -u 1 ( .g ` R ) ( 1r ` R ) ) )
19 16 18 mpan2 
 |-  ( R e. Ring -> ( Y ` -u 1 ) = ( -u 1 ( .g ` R ) ( 1r ` R ) ) )
20 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
21 16 a1i 
 |-  ( R e. Ring -> -u 1 e. ZZ )
22 9 17 20 21 10 mulgcld 
 |-  ( R e. Ring -> ( -u 1 ( .g ` R ) ( 1r ` R ) ) e. ( Base ` R ) )
23 19 22 eqeltrd 
 |-  ( R e. Ring -> ( Y ` -u 1 ) e. ( Base ` R ) )
24 23 3ad2ant1 
 |-  ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` -u 1 ) e. ( Base ` R ) )
25 fveq2 
 |-  ( ( S ` Q ) = -u 1 -> ( Y ` ( S ` Q ) ) = ( Y ` -u 1 ) )
26 25 eleq1d 
 |-  ( ( S ` Q ) = -u 1 -> ( ( Y ` ( S ` Q ) ) e. ( Base ` R ) <-> ( Y ` -u 1 ) e. ( Base ` R ) ) )
27 24 26 imbitrrid 
 |-  ( ( S ` Q ) = -u 1 -> ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) ) )
28 15 27 jaoi 
 |-  ( ( ( S ` Q ) = 1 \/ ( S ` Q ) = -u 1 ) -> ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) ) )
29 6 28 syl 
 |-  ( ( S ` Q ) e. { 1 , -u 1 } -> ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) ) )
30 5 29 mpcom 
 |-  ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) )