Theorem rngqiprngghmlem1

Description: Lemma 1 for rngqiprngghm . (Contributed by AV, 25-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 ‘ 𝐽 )
Assertion	rngqiprngghmlem1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( 1 · 𝐴 ) ∈ ( 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		eqid	⊢ ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
9	2 3 8	2idlelbas	⊢ ( 𝜑 → ( ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
10	9	simprd	⊢ ( 𝜑 → ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
11		ringrng	⊢ ( 𝐽 ∈ Ring → 𝐽 ∈ Rng )
12	4 11	syl	⊢ ( 𝜑 → 𝐽 ∈ Rng )
13	3 12	eqeltrrid	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐼 ) ∈ Rng )
14	1 2 13	rng2idl0	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐼 )
15	2 3 8	2idlbas	⊢ ( 𝜑 → ( Base ‘ 𝐽 ) = 𝐼 )
16	14 15	eleqtrrd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝐽 ) )
17	1 10 16	3jca	⊢ ( 𝜑 → ( 𝑅 ∈ Rng ∧ ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝐽 ) ) )
18	8 7	ringidcl	⊢ ( 𝐽 ∈ Ring → 1 ∈ ( Base ‘ 𝐽 ) )
19	4 18	syl	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝐽 ) )
20	19	anim1ci	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐽 ) ) )
21		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
22		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
23	21 5 6 22	rngridlmcl	⊢ ( ( ( 𝑅 ∈ Rng ∧ ( Base ‘ 𝐽 ) ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝐽 ) ) ∧ ( 𝐴 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐽 ) ) ) → ( 1 · 𝐴 ) ∈ ( Base ‘ 𝐽 ) )
24	17 20 23	syl2an2r	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐵 ) → ( 1 · 𝐴 ) ∈ ( Base ‘ 𝐽 ) )