Metamath Proof Explorer

Theorem rngqiprngfulem4

Description: Lemma 4 for rngqiprngfu . (Contributed by AV, 16-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 rngqiprngfulem4 ( 𝜑 → [ 𝑈 ] ∼ = [ 𝐸 ] ∼ )

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 14 oveq2i ⊢ ( 𝐸 − 𝑈 ) = ( 𝐸 − ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) )
16 15 a1i ⊢ ( 𝜑 → ( 𝐸 − 𝑈 ) = ( 𝐸 − ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ) )
17 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
18 1 17 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
19 1 2 3 4 5 6 7 8 9 10 11 rngqiprngfulem2 ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
20 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
21 1 20 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
22 1 2 3 4 5 6 7 rngqiprng1elbas ⊢ ( 𝜑 → 1 ∈ 𝐵 )
23 5 6 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ) → ( 1 · 𝐸 ) ∈ 𝐵 )
24 1 22 19 23 syl3anc ⊢ ( 𝜑 → ( 1 · 𝐸 ) ∈ 𝐵 )
25 5 12 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐸 ∈ 𝐵 ∧ ( 1 · 𝐸 ) ∈ 𝐵 ) → ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 )
26 21 19 24 25 syl3anc ⊢ ( 𝜑 → ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 )
27 5 13 12 18 19 26 22 ablsubsub4 ⊢ ( 𝜑 → ( ( 𝐸 − ( 𝐸 − ( 1 · 𝐸 ) ) ) − 1 ) = ( 𝐸 − ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ) )
28 5 12 18 19 24 ablnncan ⊢ ( 𝜑 → ( 𝐸 − ( 𝐸 − ( 1 · 𝐸 ) ) ) = ( 1 · 𝐸 ) )
29 28 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 − ( 𝐸 − ( 1 · 𝐸 ) ) ) − 1 ) = ( ( 1 · 𝐸 ) − 1 ) )
30 16 27 29 3eqtr2d ⊢ ( 𝜑 → ( 𝐸 − 𝑈 ) = ( ( 1 · 𝐸 ) − 1 ) )
31 ringrng ⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
32 4 31 syl ⊢ ( 𝜑 → 𝐽 ∈ Rng )
33 3 32 eqeltrrid ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
34 1 2 33 rng2idlnsg ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
35 nsgsubg ⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
36 34 35 syl ⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
37 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ) → ( 1 · 𝐸 ) ∈ ( Base ‘ 𝐽 ) )
38 19 37 mpdan ⊢ ( 𝜑 → ( 1 · 𝐸 ) ∈ ( Base ‘ 𝐽 ) )
39 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
40 2 3 39 2idlbas ⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = 𝐼 )
41 38 40 eleqtrd ⊢ ( 𝜑 → ( 1 · 𝐸 ) ∈ 𝐼 )
42 39 7 ringidcl ⊢ ( 𝐽 ∈ Ring → 1 ∈ ( Base ‘ 𝐽 ) )
43 4 42 syl ⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝐽 ) )
44 43 40 eleqtrd ⊢ ( 𝜑 → 1 ∈ 𝐼 )
45 eqid ⊢ ( -g ‘ 𝐽 ) = ( -g ‘ 𝐽 )
46 12 3 45 subgsub ⊢ ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1 · 𝐸 ) ∈ 𝐼 ∧ 1 ∈ 𝐼 ) → ( ( 1 · 𝐸 ) − 1 ) = ( ( 1 · 𝐸 ) ( -g ‘ 𝐽 ) 1 ) )
47 36 41 44 46 syl3anc ⊢ ( 𝜑 → ( ( 1 · 𝐸 ) − 1 ) = ( ( 1 · 𝐸 ) ( -g ‘ 𝐽 ) 1 ) )
48 4 ringgrpd ⊢ ( 𝜑 → 𝐽 ∈ Grp )
49 39 45 grpsubcl ⊢ ( ( 𝐽 ∈ Grp ∧ ( 1 · 𝐸 ) ∈ ( Base ‘ 𝐽 ) ∧ 1 ∈ ( Base ‘ 𝐽 ) ) → ( ( 1 · 𝐸 ) ( -g ‘ 𝐽 ) 1 ) ∈ ( Base ‘ 𝐽 ) )
50 48 38 43 49 syl3anc ⊢ ( 𝜑 → ( ( 1 · 𝐸 ) ( -g ‘ 𝐽 ) 1 ) ∈ ( Base ‘ 𝐽 ) )
51 47 50 eqeltrd ⊢ ( 𝜑 → ( ( 1 · 𝐸 ) − 1 ) ∈ ( Base ‘ 𝐽 ) )
52 51 40 eleqtrd ⊢ ( 𝜑 → ( ( 1 · 𝐸 ) − 1 ) ∈ 𝐼 )
53 30 52 eqeltrd ⊢ ( 𝜑 → ( 𝐸 − 𝑈 ) ∈ 𝐼 )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 rngqiprngfulem3 ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
55 5 12 8 qusecsub ⊢ ( ( ( 𝑅 ∈ Abel ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ) ) → ( [ 𝑈 ] ∼ = [ 𝐸 ] ∼ ↔ ( 𝐸 − 𝑈 ) ∈ 𝐼 ) )
56 18 36 54 19 55 syl22anc ⊢ ( 𝜑 → ( [ 𝑈 ] ∼ = [ 𝐸 ] ∼ ↔ ( 𝐸 − 𝑈 ) ∈ 𝐼 ) )
57 53 56 mpbird ⊢ ( 𝜑 → [ 𝑈 ] ∼ = [ 𝐸 ] ∼ )