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 = ℤRHom ⁡ R
Assertion zrhpsgnelbas ⊢ R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ S ⁡ Q ∈ Base R

Proof

Step Hyp Ref Expression
1 zrhpsgnelbas.p ⊢ P = Base SymGrp ⁡ N
2 zrhpsgnelbas.s ⊢ S = pmSgn ⁡ N
3 zrhpsgnelbas.y ⊢ Y = ℤRHom ⁡ R
4 1 2 psgnran ⊢ N ∈ Fin ∧ Q ∈ P → S ⁡ Q ∈ 1 − 1
5 4 3adant1 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → S ⁡ Q ∈ 1 − 1
6 elpri ⊢ S ⁡ Q ∈ 1 − 1 → S ⁡ Q = 1 ∨ S ⁡ Q = − 1
7 eqid ⊢ 1 R = 1 R
8 3 7 zrh1 ⊢ R ∈ Ring → Y ⁡ 1 = 1 R
9 eqid ⊢ Base R = Base R
10 9 7 ringidcl ⊢ R ∈ Ring → 1 R ∈ Base R
11 8 10 eqeltrd ⊢ R ∈ Ring → Y ⁡ 1 ∈ Base R
12 11 3ad2ant1 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ 1 ∈ Base R
13 fveq2 ⊢ S ⁡ Q = 1 → Y ⁡ S ⁡ Q = Y ⁡ 1
14 13 eleq1d ⊢ S ⁡ Q = 1 → Y ⁡ S ⁡ Q ∈ Base R ↔ Y ⁡ 1 ∈ Base R
15 12 14 syl5ibr ⊢ S ⁡ Q = 1 → R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ S ⁡ Q ∈ Base R
16 neg1z ⊢ − 1 ∈ ℤ
17 eqid ⊢ ⋅ R = ⋅ R
18 3 17 7 zrhmulg ⊢ R ∈ Ring ∧ − 1 ∈ ℤ → Y ⁡ − 1 = -1 ⋅ R 1 R
19 16 18 mpan2 ⊢ R ∈ Ring → Y ⁡ − 1 = -1 ⋅ R 1 R
20 ringgrp ⊢ R ∈ Ring → R ∈ Grp
21 16 a1i ⊢ R ∈ Ring → − 1 ∈ ℤ
22 9 17 20 21 10 mulgcld ⊢ R ∈ Ring → -1 ⋅ R 1 R ∈ Base R
23 19 22 eqeltrd ⊢ R ∈ Ring → Y ⁡ − 1 ∈ Base R
24 23 3ad2ant1 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ − 1 ∈ Base R
25 fveq2 ⊢ S ⁡ Q = − 1 → Y ⁡ S ⁡ Q = Y ⁡ − 1
26 25 eleq1d ⊢ S ⁡ Q = − 1 → Y ⁡ S ⁡ Q ∈ Base R ↔ Y ⁡ − 1 ∈ Base R
27 24 26 syl5ibr ⊢ S ⁡ Q = − 1 → R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ S ⁡ Q ∈ Base R
28 15 27 jaoi ⊢ S ⁡ Q = 1 ∨ S ⁡ Q = − 1 → R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ S ⁡ Q ∈ Base R
29 6 28 syl ⊢ S ⁡ Q ∈ 1 − 1 → R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ S ⁡ Q ∈ Base R
30 5 29 mpcom ⊢ R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ⁡ S ⁡ Q ∈ Base R