Metamath Proof Explorer

Theorem rngqiprngimfolem

Description: Lemma for rngqiprngimfo . (Contributed by AV, 5-Mar-2025) (Proof shortened by AV, 24-Mar-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 ‘ 𝐽 )
Assertion rngqiprngimfolem ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ( +g ‘ 𝑅 ) 𝐴 ) ) = 𝐴 )

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 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → 𝑅 ∈ Rng )
9 1 2 3 4 5 6 7 rngqiprng1elbas ⊢ ( 𝜑 → 1 ∈ 𝐵 )
10 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → 1 ∈ 𝐵 )
11 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
12 1 11 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
13 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → 𝑅 ∈ Grp )
14 simp3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
15 5 6 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · 𝐶 ) ∈ 𝐵 )
16 8 10 14 15 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · 𝐶 ) ∈ 𝐵 )
17 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
18 5 17 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐶 ∈ 𝐵 ∧ ( 1 · 𝐶 ) ∈ 𝐵 ) → ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ∈ 𝐵 )
19 13 14 16 18 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ∈ 𝐵 )
20 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
21 5 20 2idlss ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
22 2 21 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
23 22 sselda ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ 𝐵 )
24 23 3adant3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
25 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
26 5 25 6 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 1 ∈ 𝐵 ∧ ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ) → ( 1 · ( ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ( +g ‘ 𝑅 ) 𝐴 ) ) = ( ( 1 · ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ) ( +g ‘ 𝑅 ) ( 1 · 𝐴 ) ) )
27 8 10 19 24 26 syl13anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ( +g ‘ 𝑅 ) 𝐴 ) ) = ( ( 1 · ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ) ( +g ‘ 𝑅 ) ( 1 · 𝐴 ) ) )
28 5 6 17 8 10 14 16 rngsubdi ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ) = ( ( 1 · 𝐶 ) ( -g ‘ 𝑅 ) ( 1 · ( 1 · 𝐶 ) ) ) )
29 3 6 ressmulr ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → · = ( .r ‘ 𝐽 ) )
30 2 29 syl ⊢ ( 𝜑 → · = ( .r ‘ 𝐽 ) )
31 30 oveqd ⊢ ( 𝜑 → ( 1 · ( 1 · 𝐶 ) ) = ( 1 ( .r ‘ 𝐽 ) ( 1 · 𝐶 ) ) )
32 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( 1 · 𝐶 ) ) = ( 1 ( .r ‘ 𝐽 ) ( 1 · 𝐶 ) ) )
33 eqid ⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
34 eqid ⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝐽 )
35 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → 𝐽 ∈ Ring )
36 1 2 3 4 5 6 7 rngqiprngghmlem1 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · 𝐶 ) ∈ ( Base ‘ 𝐽 ) )
37 36 3adant2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · 𝐶 ) ∈ ( Base ‘ 𝐽 ) )
38 33 34 7 35 37 ringlidmd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝐽 ) ( 1 · 𝐶 ) ) = ( 1 · 𝐶 ) )
39 32 38 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( 1 · 𝐶 ) ) = ( 1 · 𝐶 ) )
40 39 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( ( 1 · 𝐶 ) ( -g ‘ 𝑅 ) ( 1 · ( 1 · 𝐶 ) ) ) = ( ( 1 · 𝐶 ) ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) )
41 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
42 5 41 17 grpsubid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1 · 𝐶 ) ∈ 𝐵 ) → ( ( 1 · 𝐶 ) ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) = ( 0g ‘ 𝑅 ) )
43 13 16 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( ( 1 · 𝐶 ) ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) = ( 0g ‘ 𝑅 ) )
44 28 40 43 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ) = ( 0g ‘ 𝑅 ) )
45 44 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( ( 1 · ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ) ( +g ‘ 𝑅 ) ( 1 · 𝐴 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 1 · 𝐴 ) ) )
46 5 6 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 1 · 𝐴 ) ∈ 𝐵 )
47 8 10 24 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · 𝐴 ) ∈ 𝐵 )
48 5 25 41 13 47 grplidd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 1 · 𝐴 ) ) = ( 1 · 𝐴 ) )
49 30 oveqd ⊢ ( 𝜑 → ( 1 · 𝐴 ) = ( 1 ( .r ‘ 𝐽 ) 𝐴 ) )
50 49 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · 𝐴 ) = ( 1 ( .r ‘ 𝐽 ) 𝐴 ) )
51 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ) → 𝐽 ∈ Ring )
52 2 3 33 2idlbas ⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = 𝐼 )
53 52 eqcomd ⊢ ( 𝜑 → 𝐼 = ( Base ‘ 𝐽 ) )
54 53 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ( Base ‘ 𝐽 ) ) )
55 54 biimpa ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ ( Base ‘ 𝐽 ) )
56 33 34 7 51 55 ringlidmd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ) → ( 1 ( .r ‘ 𝐽 ) 𝐴 ) = 𝐴 )
57 56 3adant3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝐽 ) 𝐴 ) = 𝐴 )
58 48 50 57 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 1 · 𝐴 ) ) = 𝐴 )
59 27 45 58 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵 ) → ( 1 · ( ( 𝐶 ( -g ‘ 𝑅 ) ( 1 · 𝐶 ) ) ( +g ‘ 𝑅 ) 𝐴 ) ) = 𝐴 )