rngqiprnglinlem1

Description: Lemma 1 for rngqiprnglin . (Contributed by AV, 28-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 = ( 1_r ‘ 𝐽 )
Assertion	rngqiprnglinlem1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) · ( 1 · 𝐶 ) ) = ( 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 = ( 1_r ‘ 𝐽 )
8	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
9	3 6	ressmulr	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → · = ( ._r ‘ 𝐽 ) )
10	8 9	syl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → · = ( ._r ‘ 𝐽 ) )
11	10	oveqd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) · 1 ) = ( ( 1 · 𝐴 ) ( ._r ‘ 𝐽 ) 1 ) )
12		eqid	⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
13		eqid	⊢ ( ._r ‘ 𝐽 ) = ( ._r ‘ 𝐽 )
14	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐽 ∈ Ring )
15	1 2 3 4 5 6 7	rngqiprngghmlem1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( 1 · 𝐴 ) ∈ ( Base ‘ 𝐽 ) )
16	15	adantrr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 · 𝐴 ) ∈ ( Base ‘ 𝐽 ) )
17	12 13 7 14 16	ringridmd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) ( ._r ‘ 𝐽 ) 1 ) = ( 1 · 𝐴 ) )
18	11 17	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) · 1 ) = ( 1 · 𝐴 ) )
19	18	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 1 · 𝐴 ) · 1 ) · 𝐶 ) = ( ( 1 · 𝐴 ) · 𝐶 ) )
20	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝑅 ∈ Rng )
21	1 2 3 4 5 6 7	rngqiprng1elbas	⊢ ( 𝜑 → 1 ∈ 𝐵 )
22	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 1 ∈ 𝐵 )
23		simprl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 )
24	5 6	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 1 · 𝐴 ) ∈ 𝐵 )
25	20 22 23 24	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 1 · 𝐴 ) ∈ 𝐵 )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
27	5 6	rngass	⊢ ( ( 𝑅 ∈ Rng ∧ ( ( 1 · 𝐴 ) ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 1 · 𝐴 ) · 1 ) · 𝐶 ) = ( ( 1 · 𝐴 ) · ( 1 · 𝐶 ) ) )
28	20 25 22 26 27	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 1 · 𝐴 ) · 1 ) · 𝐶 ) = ( ( 1 · 𝐴 ) · ( 1 · 𝐶 ) ) )
29	5 6	rngass	⊢ ( ( 𝑅 ∈ Rng ∧ ( 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) · 𝐶 ) = ( 1 · ( 𝐴 · 𝐶 ) ) )
30	20 22 23 26 29	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) · 𝐶 ) = ( 1 · ( 𝐴 · 𝐶 ) ) )
31	19 28 30	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 · 𝐴 ) · ( 1 · 𝐶 ) ) = ( 1 · ( 𝐴 · 𝐶 ) ) )

Metamath Proof Explorer

Theorem rngqiprnglinlem1

Proof