Metamath Proof Explorer

Theorem rngqiprngfulem5

Description: Lemma 5 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 rngqiprngfulem5 ( 𝜑 → ( 1 · 𝑈 ) = 1 )

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 · ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) )
16 15 a1i ⊢ ( 𝜑 → ( 1 · 𝑈 ) = ( 1 · ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ) )
17 1 2 3 4 5 6 7 rngqiprng1elbas ⊢ ( 𝜑 → 1 ∈ 𝐵 )
18 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
19 1 18 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
20 1 2 3 4 5 6 7 8 9 10 11 rngqiprngfulem2 ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
21 5 6 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ) → ( 1 · 𝐸 ) ∈ 𝐵 )
22 1 17 20 21 syl3anc ⊢ ( 𝜑 → ( 1 · 𝐸 ) ∈ 𝐵 )
23 5 12 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐸 ∈ 𝐵 ∧ ( 1 · 𝐸 ) ∈ 𝐵 ) → ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 )
24 19 20 22 23 syl3anc ⊢ ( 𝜑 → ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 )
25 5 13 6 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 1 ∈ 𝐵 ∧ ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 ∧ 1 ∈ 𝐵 ) ) → ( 1 · ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ) = ( ( 1 · ( 𝐸 − ( 1 · 𝐸 ) ) ) + ( 1 · 1 ) ) )
26 1 17 24 17 25 syl13anc ⊢ ( 𝜑 → ( 1 · ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ) = ( ( 1 · ( 𝐸 − ( 1 · 𝐸 ) ) ) + ( 1 · 1 ) ) )
27 5 6 12 1 17 20 22 rngsubdi ⊢ ( 𝜑 → ( 1 · ( 𝐸 − ( 1 · 𝐸 ) ) ) = ( ( 1 · 𝐸 ) − ( 1 · ( 1 · 𝐸 ) ) ) )
28 5 6 rngass ⊢ ( ( 𝑅 ∈ Rng ∧ ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ) ) → ( ( 1 · 1 ) · 𝐸 ) = ( 1 · ( 1 · 𝐸 ) ) )
29 1 17 17 20 28 syl13anc ⊢ ( 𝜑 → ( ( 1 · 1 ) · 𝐸 ) = ( 1 · ( 1 · 𝐸 ) ) )
30 3 6 ressmulr ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → · = ( .r ‘ 𝐽 ) )
31 2 30 syl ⊢ ( 𝜑 → · = ( .r ‘ 𝐽 ) )
32 31 oveqd ⊢ ( 𝜑 → ( 1 · 1 ) = ( 1 ( .r ‘ 𝐽 ) 1 ) )
33 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
34 33 7 ringidcl ⊢ ( 𝐽 ∈ Ring → 1 ∈ ( Base ‘ 𝐽 ) )
35 eqid ⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
36 33 35 7 ringlidm ⊢ ( ( 𝐽 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝐽 ) ) → ( 1 ( .r ‘ 𝐽 ) 1 ) = 1 )
37 4 34 36 syl2anc2 ⊢ ( 𝜑 → ( 1 ( .r ‘ 𝐽 ) 1 ) = 1 )
38 32 37 eqtrd ⊢ ( 𝜑 → ( 1 · 1 ) = 1 )
39 38 oveq1d ⊢ ( 𝜑 → ( ( 1 · 1 ) · 𝐸 ) = ( 1 · 𝐸 ) )
40 29 39 eqtr3d ⊢ ( 𝜑 → ( 1 · ( 1 · 𝐸 ) ) = ( 1 · 𝐸 ) )
41 40 oveq2d ⊢ ( 𝜑 → ( ( 1 · 𝐸 ) − ( 1 · ( 1 · 𝐸 ) ) ) = ( ( 1 · 𝐸 ) − ( 1 · 𝐸 ) ) )
42 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
43 5 42 12 grpsubid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1 · 𝐸 ) ∈ 𝐵 ) → ( ( 1 · 𝐸 ) − ( 1 · 𝐸 ) ) = ( 0g ‘ 𝑅 ) )
44 19 22 43 syl2anc ⊢ ( 𝜑 → ( ( 1 · 𝐸 ) − ( 1 · 𝐸 ) ) = ( 0g ‘ 𝑅 ) )
45 27 41 44 3eqtrd ⊢ ( 𝜑 → ( 1 · ( 𝐸 − ( 1 · 𝐸 ) ) ) = ( 0g ‘ 𝑅 ) )
46 45 38 oveq12d ⊢ ( 𝜑 → ( ( 1 · ( 𝐸 − ( 1 · 𝐸 ) ) ) + ( 1 · 1 ) ) = ( ( 0g ‘ 𝑅 ) + 1 ) )
47 26 46 eqtrd ⊢ ( 𝜑 → ( 1 · ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ) = ( ( 0g ‘ 𝑅 ) + 1 ) )
48 5 13 42 19 17 grplidd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + 1 ) = 1 )
49 16 47 48 3eqtrd ⊢ ( 𝜑 → ( 1 · 𝑈 ) = 1 )