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 ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝑆 ∈ Ring )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝑆 ∈ Rng )
2 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
4 2 3 rngisomfv1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑆 ) )
5 4 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑆 ) )
6 oveq1 ⊢ ( 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) → ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) )
7 6 eqeq1d ⊢ ( 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) → ( ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ↔ ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ) )
8 oveq2 ⊢ ( 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) )
9 8 eqeq1d ⊢ ( 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = 𝑥 ↔ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) )
10 7 9 anbi12d ⊢ ( 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = 𝑥 ) ↔ ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) )
11 10 ralbidv ⊢ ( 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) )
12 11 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ 𝑖 = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) )
13 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
14 2 3 13 rngisom1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) )
15 5 12 14 rspcedvd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ∃ 𝑖 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = 𝑥 ) )
16 3 13 isringrng ⊢ ( 𝑆 ∈ Ring ↔ ( 𝑆 ∈ Rng ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑆 ) ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝑖 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) 𝑖 ) = 𝑥 ) ) )
17 1 15 16 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝑆 ∈ Ring )