Theorem rngqiprngghmlem3

Description: Lemma 3 for rngqiprngghm . (Contributed by AV, 25-Feb-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	rngqiprngghmlem3	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 · ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ) = ( ( 1 · 𝐴 ) ( +g ‘ 𝐽 ) ( 1 · 𝐶 ) ) )

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 2 3 4 5 6 7	rngqiprng1elbas	⊢ ( 𝜑 → 1 ∈ 𝐵 )
9	8	anim1i	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
10		3anass	⊢ ( ( 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ↔ ( 1 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
11	9 10	sylibr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) )
12		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
13	5 12 6	rngdi	⊢ ( ( 𝑅 ∈ Rng ∧ ( 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 · ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ) = ( ( 1 · 𝐴 ) ( +g ‘ 𝑅 ) ( 1 · 𝐶 ) ) )
14	1 11 13	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 · ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ) = ( ( 1 · 𝐴 ) ( +g ‘ 𝑅 ) ( 1 · 𝐶 ) ) )
15	3 12	ressplusg	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐽 ) )
16	2 15	syl	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐽 ) )
17	16	oveqd	⊢ ( 𝜑 → ( ( 1 · 𝐴 ) ( +g ‘ 𝑅 ) ( 1 · 𝐶 ) ) = ( ( 1 · 𝐴 ) ( +g ‘ 𝐽 ) ( 1 · 𝐶 ) ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) ( +g ‘ 𝑅 ) ( 1 · 𝐶 ) ) = ( ( 1 · 𝐴 ) ( +g ‘ 𝐽 ) ( 1 · 𝐶 ) ) )
19	14 18	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 · ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ) = ( ( 1 · 𝐴 ) ( +g ‘ 𝐽 ) ( 1 · 𝐶 ) ) )