This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
zrhpsgnelbas.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
zrhpsgnelbas.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
Assertion zrhpsgnelbas ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 zrhpsgnelbas.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 zrhpsgnelbas.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3 zrhpsgnelbas.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
4 1 2 psgnran ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } )
5 4 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } )
6 elpri ⊢ ( ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } → ( ( 𝑆 ‘ 𝑄 ) = 1 ∨ ( 𝑆 ‘ 𝑄 ) = - 1 ) )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 3 7 zrh1 ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ 1 ) = ( 1r ‘ 𝑅 ) )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 7 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11 8 10 eqeltrd ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
12 11 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
13 fveq2 ⊢ ( ( 𝑆 ‘ 𝑄 ) = 1 → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) = ( 𝑌 ‘ 1 ) )
14 13 eleq1d ⊢ ( ( 𝑆 ‘ 𝑄 ) = 1 → ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ↔ ( 𝑌 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) ) )
15 12 14 imbitrrid ⊢ ( ( 𝑆 ‘ 𝑄 ) = 1 → ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ) )
16 neg1z ⊢ - 1 ∈ ℤ
17 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
18 3 17 7 zrhmulg ⊢ ( ( 𝑅 ∈ Ring ∧ - 1 ∈ ℤ ) → ( 𝑌 ‘ - 1 ) = ( - 1 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
19 16 18 mpan2 ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ - 1 ) = ( - 1 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
20 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
21 16 a1i ⊢ ( 𝑅 ∈ Ring → - 1 ∈ ℤ )
22 9 17 20 21 10 mulgcld ⊢ ( 𝑅 ∈ Ring → ( - 1 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
23 19 22 eqeltrd ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ - 1 ) ∈ ( Base ‘ 𝑅 ) )
24 23 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ - 1 ) ∈ ( Base ‘ 𝑅 ) )
25 fveq2 ⊢ ( ( 𝑆 ‘ 𝑄 ) = - 1 → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) = ( 𝑌 ‘ - 1 ) )
26 25 eleq1d ⊢ ( ( 𝑆 ‘ 𝑄 ) = - 1 → ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ↔ ( 𝑌 ‘ - 1 ) ∈ ( Base ‘ 𝑅 ) ) )
27 24 26 imbitrrid ⊢ ( ( 𝑆 ‘ 𝑄 ) = - 1 → ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ) )
28 15 27 jaoi ⊢ ( ( ( 𝑆 ‘ 𝑄 ) = 1 ∨ ( 𝑆 ‘ 𝑄 ) = - 1 ) → ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ) )
29 6 28 syl ⊢ ( ( 𝑆 ‘ 𝑄 ) ∈ { 1 , - 1 } → ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) ) )
30 5 29 mpcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) )