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 )