Metamath Proof Explorer

Theorem rngisomring1

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the ring unity of the second ring is the function value of the ring unity of the first ring for the isomorphism. (Contributed by AV, 16-Mar-2025)

Ref Expression
Assertion rngisomring1 ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 1r ‘ 𝑆 ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
3 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
4 1 2 3 rngisom1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) )
5 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
6 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 7 2 rngimf1o ⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) )
9 f1of ⊢ ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
10 8 9 syl ⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
11 10 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
12 7 1 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
13 12 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
14 11 13 ffvelcdmd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑆 ) )
15 14 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑆 ) )
16 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) )
17 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
18 16 17 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ↔ ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ) )
19 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) )
20 19 17 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ↔ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) )
21 18 20 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ↔ ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) ) )
22 21 rspccv ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) → ( 𝑦 ∈ ( Base ‘ 𝑆 ) → ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) ) )
23 22 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑆 ) → ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) ) )
24 simpl ⊢ ( ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) → ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 )
25 23 24 syl6 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑆 ) → ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ) )
26 25 imp ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 )
27 simpr ⊢ ( ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) → ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 )
28 23 27 syl6 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑆 ) → ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 ) )
29 28 imp ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑦 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑦 )
30 5 6 15 26 29 ringurd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = 𝑥 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
31 4 30 mpdan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
32 31 eqcomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Rng ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ( 1r ‘ 𝑆 ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )