Metamath Proof Explorer

Theorem pzriprnglem7

Description: Lemma 7 for pzriprng : J is a unital ring. (Contributed by AV, 19-Mar-2025)

Ref Expression
Hypotheses pzriprng.r ⊢ R = ℤ ring × 𝑠 ℤ ring
pzriprng.i ⊢ I = ℤ × 0
pzriprng.j ⊢ J = R ↾ 𝑠 I
Assertion pzriprnglem7 ⊢ J ∈ Ring

Proof

Step Hyp Ref Expression
1 pzriprng.r ⊢ R = ℤ ring × 𝑠 ℤ ring
2 pzriprng.i ⊢ I = ℤ × 0
3 pzriprng.j ⊢ J = R ↾ 𝑠 I
4 1 2 pzriprnglem5 ⊢ I ∈ SubRng ⁡ R
5 3 subrngrng ⊢ I ∈ SubRng ⁡ R → J ∈ Rng
6 4 5 ax-mp ⊢ J ∈ Rng
7 1z ⊢ 1 ∈ ℤ
8 c0ex ⊢ 0 ∈ V
9 8 snid ⊢ 0 ∈ 0
10 7 9 opelxpii ⊢ 1 0 ∈ ℤ × 0
11 3 subrngbas ⊢ I ∈ SubRng ⁡ R → I = Base J
12 4 11 ax-mp ⊢ I = Base J
13 12 2 eqtr3i ⊢ Base J = ℤ × 0
14 10 13 eleqtrri ⊢ 1 0 ∈ Base J
15 oveq1 ⊢ i = 1 0 → i ⋅ J x = 1 0 ⋅ J x
16 15 eqeq1d ⊢ i = 1 0 → i ⋅ J x = x ↔ 1 0 ⋅ J x = x
17 16 ovanraleqv ⊢ i = 1 0 → ∀ x ∈ Base J i ⋅ J x = x ∧ x ⋅ J i = x ↔ ∀ x ∈ Base J 1 0 ⋅ J x = x ∧ x ⋅ J 1 0 = x
18 id ⊢ 1 0 ∈ Base J → 1 0 ∈ Base J
19 12 eleq2i ⊢ x ∈ I ↔ x ∈ Base J
20 1 2 3 pzriprnglem6 ⊢ x ∈ I → 1 0 ⋅ J x = x ∧ x ⋅ J 1 0 = x
21 19 20 sylbir ⊢ x ∈ Base J → 1 0 ⋅ J x = x ∧ x ⋅ J 1 0 = x
22 21 a1i ⊢ 1 0 ∈ Base J → x ∈ Base J → 1 0 ⋅ J x = x ∧ x ⋅ J 1 0 = x
23 22 ralrimiv ⊢ 1 0 ∈ Base J → ∀ x ∈ Base J 1 0 ⋅ J x = x ∧ x ⋅ J 1 0 = x
24 17 18 23 rspcedvdw ⊢ 1 0 ∈ Base J → ∃ i ∈ Base J ∀ x ∈ Base J i ⋅ J x = x ∧ x ⋅ J i = x
25 14 24 ax-mp ⊢ ∃ i ∈ Base J ∀ x ∈ Base J i ⋅ J x = x ∧ x ⋅ J i = x
26 eqid ⊢ Base J = Base J
27 eqid ⊢ ⋅ J = ⋅ J
28 26 27 isringrng ⊢ J ∈ Ring ↔ J ∈ Rng ∧ ∃ i ∈ Base J ∀ x ∈ Base J i ⋅ J x = x ∧ x ⋅ J i = x
29 6 25 28 mpbir2an ⊢ J ∈ Ring