Metamath Proof Explorer

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 ‘ 𝑄 ) [ 𝐶 ] ∼ ) )