Metamath Proof Explorer

Theorem rngqiprngu

Description: If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025)

Ref Expression
Hypotheses rngqiprngfu.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rngqiprngfu.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
rngqiprngfu.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
rngqiprngfu.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
rngqiprngfu.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rngqiprngfu.t ⊢ · = ( .r ‘ 𝑅 )
rngqiprngfu.1 ⊢ 1 = ( 1r ‘ 𝐽 )
rngqiprngfu.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
rngqiprngfu.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
rngqiprngfu.v ⊢ ( 𝜑 → 𝑄 ∈ Ring )
rngqiprngfu.e ⊢ ( 𝜑 → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
rngqiprngfu.m ⊢ − = ( -g ‘ 𝑅 )
rngqiprngfu.a ⊢ + = ( +g ‘ 𝑅 )
rngqiprngfu.n ⊢ 𝑈 = ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 )
Assertion rngqiprngu ( 𝜑 → ( 1r ‘ 𝑅 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 rngqiprngfu.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
2 rngqiprngfu.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3 rngqiprngfu.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 rngqiprngfu.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
5 rngqiprngfu.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 rngqiprngfu.t ⊢ · = ( .r ‘ 𝑅 )
7 rngqiprngfu.1 ⊢ 1 = ( 1r ‘ 𝐽 )
8 rngqiprngfu.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9 rngqiprngfu.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
10 rngqiprngfu.v ⊢ ( 𝜑 → 𝑄 ∈ Ring )
11 rngqiprngfu.e ⊢ ( 𝜑 → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
12 rngqiprngfu.m ⊢ − = ( -g ‘ 𝑅 )
13 rngqiprngfu.a ⊢ + = ( +g ‘ 𝑅 )
14 rngqiprngfu.n ⊢ 𝑈 = ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 )
15 eqid ⊢ ( 𝑄 ×s 𝐽 ) = ( 𝑄 ×s 𝐽 )
16 15 10 4 xpsringd ⊢ ( 𝜑 → ( 𝑄 ×s 𝐽 ) ∈ Ring )
17 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
18 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
19 1 2 3 4 5 6 7 8 9 17 15 18 rngqiprngim ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ∈ ( 𝑅 RngIso ( 𝑄 ×s 𝐽 ) ) )
20 rngimcnv ⊢ ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ∈ ( 𝑅 RngIso ( 𝑄 ×s 𝐽 ) ) → ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ∈ ( ( 𝑄 ×s 𝐽 ) RngIso 𝑅 ) )
21 19 20 syl ⊢ ( 𝜑 → ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ∈ ( ( 𝑄 ×s 𝐽 ) RngIso 𝑅 ) )
22 rngisomring1 ⊢ ( ( ( 𝑄 ×s 𝐽 ) ∈ Ring ∧ 𝑅 ∈ Rng ∧ ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ∈ ( ( 𝑄 ×s 𝐽 ) RngIso 𝑅 ) ) → ( 1r ‘ 𝑅 ) = ( ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ) )
23 16 1 21 22 syl3anc ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ) )
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 18 rngqiprngfu ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ 𝑈 ) = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 rngqipring1 ⊢ ( 𝜑 → ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) = ⟨ [ 𝐸 ] ∼ , 1 ⟩ )
26 24 25 eqtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ 𝑈 ) = ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) )
27 eqid ⊢ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) = ( Base ‘ ( 𝑄 ×s 𝐽 ) )
28 5 27 rngimf1o ⊢ ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ∈ ( 𝑅 RngIso ( 𝑄 ×s 𝐽 ) ) → ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) : 𝐵 –1-1-onto→ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) )
29 19 28 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) : 𝐵 –1-1-onto→ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) )
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 rngqiprngfulem3 ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
31 eqid ⊢ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) = ( 1r ‘ ( 𝑄 ×s 𝐽 ) )
32 27 31 ringidcl ⊢ ( ( 𝑄 ×s 𝐽 ) ∈ Ring → ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ∈ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) )
33 16 32 syl ⊢ ( 𝜑 → ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ∈ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) )
34 f1ocnvfvb ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) : 𝐵 –1-1-onto→ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) ∧ 𝑈 ∈ 𝐵 ∧ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ∈ ( Base ‘ ( 𝑄 ×s 𝐽 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ 𝑈 ) = ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ↔ ( ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ) = 𝑈 ) )
35 29 30 33 34 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ 𝑈 ) = ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ↔ ( ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ) = 𝑈 ) )
36 26 35 mpbid ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ ) ‘ ( 1r ‘ ( 𝑄 ×s 𝐽 ) ) ) = 𝑈 )
37 23 36 eqtrd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = 𝑈 )