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

Metamath Proof Explorer

Theorem rngisomring

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then both rings are unital. (Contributed by AV, 27-Feb-2025)

Ref Expression
Assertion rngisomring ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S → S ∈ Ring

Proof

Step Hyp Ref Expression
1 simp2 ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S → S ∈ Rng
2 eqid ⊢ 1 R = 1 R
3 eqid ⊢ Base S = Base S
4 2 3 rngisomfv1 ⊢ R ∈ Ring ∧ F ∈ R RngIso S → F ⁡ 1 R ∈ Base S
5 4 3adant2 ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S → F ⁡ 1 R ∈ Base S
6 oveq1 ⊢ i = F ⁡ 1 R → i ⋅ S x = F ⁡ 1 R ⋅ S x
7 6 eqeq1d ⊢ i = F ⁡ 1 R → i ⋅ S x = x ↔ F ⁡ 1 R ⋅ S x = x
8 oveq2 ⊢ i = F ⁡ 1 R → x ⋅ S i = x ⋅ S F ⁡ 1 R
9 8 eqeq1d ⊢ i = F ⁡ 1 R → x ⋅ S i = x ↔ x ⋅ S F ⁡ 1 R = x
10 7 9 anbi12d ⊢ i = F ⁡ 1 R → i ⋅ S x = x ∧ x ⋅ S i = x ↔ F ⁡ 1 R ⋅ S x = x ∧ x ⋅ S F ⁡ 1 R = x
11 10 ralbidv ⊢ i = F ⁡ 1 R → ∀ x ∈ Base S i ⋅ S x = x ∧ x ⋅ S i = x ↔ ∀ x ∈ Base S F ⁡ 1 R ⋅ S x = x ∧ x ⋅ S F ⁡ 1 R = x
12 11 adantl ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S ∧ i = F ⁡ 1 R → ∀ x ∈ Base S i ⋅ S x = x ∧ x ⋅ S i = x ↔ ∀ x ∈ Base S F ⁡ 1 R ⋅ S x = x ∧ x ⋅ S F ⁡ 1 R = x
13 eqid ⊢ ⋅ S = ⋅ S
14 2 3 13 rngisom1 ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S → ∀ x ∈ Base S F ⁡ 1 R ⋅ S x = x ∧ x ⋅ S F ⁡ 1 R = x
15 5 12 14 rspcedvd ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S → ∃ i ∈ Base S ∀ x ∈ Base S i ⋅ S x = x ∧ x ⋅ S i = x
16 3 13 isringrng ⊢ S ∈ Ring ↔ S ∈ Rng ∧ ∃ i ∈ Base S ∀ x ∈ Base S i ⋅ S x = x ∧ x ⋅ S i = x
17 1 15 16 sylanbrc ⊢ R ∈ Ring ∧ S ∈ Rng ∧ F ∈ R RngIso S → S ∈ Ring