Theorem rngqiprnglinlem2

Description: Lemma 2 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	rngqiprnglinlem2	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 · 𝐶 ) ] ∼ = ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) )

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		ringrng	⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
11	4 10	syl	⊢ ( 𝜑 → 𝐽 ∈ Rng )
12	3 11	eqeltrrid	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
13	1 2 12	rng2idlsubrng	⊢ ( 𝜑 → 𝐼 ∈ ( SubRng ‘ 𝑅 ) )
14		subrngsubg	⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
15	13 14	syl	⊢ ( 𝜑 → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
16	1 2 15	3jca	⊢ ( 𝜑 → ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) )
17		eqid	⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
18	8	oveq2i	⊢ ( 𝑅 /s ∼ ) = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
19	9 18	eqtri	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
20		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
21	17 19 5 6 20	qusmulrng	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝐶 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝐴 · 𝐶 ) ] ( 𝑅 ~QG 𝐼 ) )
22	16 21	sylan	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝐶 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝐴 · 𝐶 ) ] ( 𝑅 ~QG 𝐼 ) )
23	8	eceq2i	⊢ [ 𝐴 ] ∼ = [ 𝐴 ] ( 𝑅 ~QG 𝐼 )
24	8	eceq2i	⊢ [ 𝐶 ] ∼ = [ 𝐶 ] ( 𝑅 ~QG 𝐼 )
25	23 24	oveq12i	⊢ ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) = ( [ 𝐴 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝐶 ] ( 𝑅 ~QG 𝐼 ) )
26	8	eceq2i	⊢ [ ( 𝐴 · 𝐶 ) ] ∼ = [ ( 𝐴 · 𝐶 ) ] ( 𝑅 ~QG 𝐼 )
27	22 25 26	3eqtr4g	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) = [ ( 𝐴 · 𝐶 ) ] ∼ )
28	27	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 · 𝐶 ) ] ∼ = ( [ 𝐴 ] ∼ ( .r ‘ 𝑄 ) [ 𝐶 ] ∼ ) )