Theorem rngqiprnglinlem3

Description: Lemma 3 for rngqiprnglin . (Contributed by AV, 28-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 ∼ )
Assertion	rngqiprnglinlem3	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) ∈ ( Base ‘ 𝑄 ) )

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	1 2 3 4 5 6 7 8 9	rngqiprnglinlem2	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 · 𝐶 ) ] ∼ = ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) )
11	1	anim1i	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
12		3anass	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
13	11 12	sylibr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝑅 ∈ Rng ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) )
14	5 6	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐴 · 𝐶 ) ∈ 𝐵 )
15	13 14	syl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐴 · 𝐶 ) ∈ 𝐵 )
16		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
17	8 9 5 16	quseccl0	⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 · 𝐶 ) ∈ 𝐵 ) → [ ( 𝐴 · 𝐶 ) ] ∼ ∈ ( Base ‘ 𝑄 ) )
18	1 15 17	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 · 𝐶 ) ] ∼ ∈ ( Base ‘ 𝑄 ) )
19	10 18	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) ∈ ( Base ‘ 𝑄 ) )