Metamath Proof Explorer

Theorem rngqiprngghm

Description: F is a homomorphism of the additive groups of non-unital rings. (Contributed by AV, 24-Feb-2025)

Ref Expression
Hypotheses rng2idlring.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rng2idlring.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
rng2idlring.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
rng2idlring.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
rng2idlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rng2idlring.t ⊢ · = ( .r ‘ 𝑅 )
rng2idlring.1 ⊢ 1 = ( 1r ‘ 𝐽 )
rngqiprngim.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
rngqiprngim.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
rngqiprngim.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
rngqiprngim.p ⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
rngqiprngim.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
Assertion rngqiprngghm ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑃 ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
2 rng2idlring.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3 rng2idlring.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 rng2idlring.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
5 rng2idlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 rng2idlring.t ⊢ · = ( .r ‘ 𝑅 )
7 rng2idlring.1 ⊢ 1 = ( 1r ‘ 𝐽 )
8 rngqiprngim.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9 rngqiprngim.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
10 rngqiprngim.c ⊢ 𝐶 = ( Base ‘ 𝑄 )
11 rngqiprngim.p ⊢ 𝑃 = ( 𝑄 ×s 𝐽 )
12 rngqiprngim.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ [ 𝑥 ] ∼ , ( 1 · 𝑥 ) ⟩ )
13 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
15 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
16 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
17 1 16 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
18 1 2 3 4 5 6 7 8 9 10 11 rngqiprng ⊢ ( 𝜑 → 𝑃 ∈ Rng )
19 rnggrp ⊢ ( 𝑃 ∈ Rng → 𝑃 ∈ Grp )
20 18 19 syl ⊢ ( 𝜑 → 𝑃 ∈ Grp )
21 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimf ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 𝐶 × 𝐼 ) )
22 1 2 3 4 5 6 7 8 9 10 11 rngqipbas ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( 𝐶 × 𝐼 ) )
23 22 feq3d ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑃 ) ↔ 𝐹 : 𝐵 ⟶ ( 𝐶 × 𝐼 ) ) )
24 21 23 mpbird ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
25 ringrng ⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
26 4 25 syl ⊢ ( 𝜑 → 𝐽 ∈ Rng )
27 3 26 eqeltrrid ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
28 1 2 27 rng2idlnsg ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
29 28 5 8 9 ecqusaddd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ] ∼ = ( [ 𝑎 ] ∼ ( +g ‘ 𝑄 ) [ 𝑏 ] ∼ ) )
30 1 2 3 4 5 6 7 rngqiprngghmlem3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 1 · ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 1 · 𝑎 ) ( +g ‘ 𝐽 ) ( 1 · 𝑏 ) ) )
31 29 30 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ⟨ [ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ] ∼ , ( 1 · ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) ⟩ = ⟨ ( [ 𝑎 ] ∼ ( +g ‘ 𝑄 ) [ 𝑏 ] ∼ ) , ( ( 1 · 𝑎 ) ( +g ‘ 𝐽 ) ( 1 · 𝑏 ) ) ⟩ )
32 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
33 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
34 9 ovexi ⊢ 𝑄 ∈ V
35 34 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑄 ∈ V )
36 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐽 ∈ Ring )
37 simpl ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
38 8 9 5 32 quseccl0 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ) → [ 𝑎 ] ∼ ∈ ( Base ‘ 𝑄 ) )
39 1 37 38 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ 𝑎 ] ∼ ∈ ( Base ‘ 𝑄 ) )
40 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 1 · 𝑎 ) ∈ ( Base ‘ 𝐽 ) )
41 40 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 1 · 𝑎 ) ∈ ( Base ‘ 𝐽 ) )
42 simpr ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
43 8 9 5 32 quseccl0 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑏 ∈ 𝐵 ) → [ 𝑏 ] ∼ ∈ ( Base ‘ 𝑄 ) )
44 1 42 43 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ 𝑏 ] ∼ ∈ ( Base ‘ 𝑄 ) )
45 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 · 𝑏 ) ∈ ( Base ‘ 𝐽 ) )
46 45 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 1 · 𝑏 ) ∈ ( Base ‘ 𝐽 ) )
47 28 5 8 9 ecqusaddcl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( [ 𝑎 ] ∼ ( +g ‘ 𝑄 ) [ 𝑏 ] ∼ ) ∈ ( Base ‘ 𝑄 ) )
48 1 2 3 4 5 6 7 rngqiprngghmlem2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 1 · 𝑎 ) ( +g ‘ 𝐽 ) ( 1 · 𝑏 ) ) ∈ ( Base ‘ 𝐽 ) )
49 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
50 eqid ⊢ ( +g ‘ 𝐽 ) = ( +g ‘ 𝐽 )
51 11 32 33 35 36 39 41 44 46 47 48 49 50 15 xpsadd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ( +g ‘ 𝑃 ) ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ ) = ⟨ ( [ 𝑎 ] ∼ ( +g ‘ 𝑄 ) [ 𝑏 ] ∼ ) , ( ( 1 · 𝑎 ) ( +g ‘ 𝐽 ) ( 1 · 𝑏 ) ) ⟩ )
52 31 51 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ⟨ [ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ] ∼ , ( 1 · ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) ⟩ = ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ( +g ‘ 𝑃 ) ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ ) )
53 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑅 ∈ Rng )
54 37 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
55 42 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
56 5 14 rngacl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
57 53 54 55 56 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
58 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ⟨ [ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ] ∼ , ( 1 · ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) ⟩ )
59 57 58 syldan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ⟨ [ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ] ∼ , ( 1 · ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) ⟩ )
60 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
61 60 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑎 ) = ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ )
62 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) = ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ )
63 62 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) = ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ )
64 61 63 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑃 ) ( 𝐹 ‘ 𝑏 ) ) = ( ⟨ [ 𝑎 ] ∼ , ( 1 · 𝑎 ) ⟩ ( +g ‘ 𝑃 ) ⟨ [ 𝑏 ] ∼ , ( 1 · 𝑏 ) ⟩ ) )
65 52 59 64 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑃 ) ( 𝐹 ‘ 𝑏 ) ) )
66 5 13 14 15 17 20 24 65 isghmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑃 ) )