Theorem rngqiprngghmlem1

Description: Lemma 1 for rngqiprngghm . (Contributed by AV, 25-Feb-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	|- ( ph -> R e. Rng )
	rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlring.j	|- J = ( R |`s I )
	rng2idlring.u	|- ( ph -> J e. Ring )
	rng2idlring.b	|- B = ( Base ` R )
	rng2idlring.t	|- .x. = ( .r ` R )
	rng2idlring.1	|- .1. = ( 1r ` J )
Assertion	rngqiprngghmlem1	|- ( ( ph /\ A e. B ) -> ( .1. .x. A ) e. ( Base ` J ) )

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	|- ( ph -> R e. Rng )
2		rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idlring.j	|- J = ( R |`s I )
4		rng2idlring.u	|- ( ph -> J e. Ring )
5		rng2idlring.b	|- B = ( Base ` R )
6		rng2idlring.t	|- .x. = ( .r ` R )
7		rng2idlring.1	|- .1. = ( 1r ` J )
8		eqid	|- ( Base ` J ) = ( Base ` J )
9	2 3 8	2idlelbas	|- ( ph -> ( ( Base ` J ) e. ( LIdeal ` R ) /\ ( Base ` J ) e. ( LIdeal ` ( oppR ` R ) ) ) )
10	9	simprd	|- ( ph -> ( Base ` J ) e. ( LIdeal ` ( oppR ` R ) ) )
11		ringrng	|- ( J e. Ring -> J e. Rng )
12	4 11	syl	|- ( ph -> J e. Rng )
13	3 12	eqeltrrid	|- ( ph -> ( R |`s I ) e. Rng )
14	1 2 13	rng2idl0	|- ( ph -> ( 0g ` R ) e. I )
15	2 3 8	2idlbas	|- ( ph -> ( Base ` J ) = I )
16	14 15	eleqtrrd	|- ( ph -> ( 0g ` R ) e. ( Base ` J ) )
17	1 10 16	3jca	|- ( ph -> ( R e. Rng /\ ( Base ` J ) e. ( LIdeal ` ( oppR ` R ) ) /\ ( 0g ` R ) e. ( Base ` J ) ) )
18	8 7	ringidcl	|- ( J e. Ring -> .1. e. ( Base ` J ) )
19	4 18	syl	|- ( ph -> .1. e. ( Base ` J ) )
20	19	anim1ci	|- ( ( ph /\ A e. B ) -> ( A e. B /\ .1. e. ( Base ` J ) ) )
21		eqid	|- ( 0g ` R ) = ( 0g ` R )
22		eqid	|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
23	21 5 6 22	rngridlmcl	|- ( ( ( R e. Rng /\ ( Base ` J ) e. ( LIdeal ` ( oppR ` R ) ) /\ ( 0g ` R ) e. ( Base ` J ) ) /\ ( A e. B /\ .1. e. ( Base ` J ) ) ) -> ( .1. .x. A ) e. ( Base ` J ) )
24	17 20 23	syl2an2r	|- ( ( ph /\ A e. B ) -> ( .1. .x. A ) e. ( Base ` J ) )