Theorem rngqiprngghmlem2

Description: Lemma 2 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	rngqiprngghmlem2	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) 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		ringrng	|- ( J e. Ring -> J e. Rng )
9	4 8	syl	|- ( ph -> J e. Rng )
10	9	adantr	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> J e. Rng )
11	1 2 3 4 5 6 7	rngqiprngghmlem1	|- ( ( ph /\ A e. B ) -> ( .1. .x. A ) e. ( Base ` J ) )
12	11	adantrr	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. A ) e. ( Base ` J ) )
13	1 2 3 4 5 6 7	rngqiprngghmlem1	|- ( ( ph /\ C e. B ) -> ( .1. .x. C ) e. ( Base ` J ) )
14	13	adantrl	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. C ) e. ( Base ` J ) )
15		eqid	|- ( Base ` J ) = ( Base ` J )
16		eqid	|- ( +g ` J ) = ( +g ` J )
17	15 16	rngacl	|- ( ( J e. Rng /\ ( .1. .x. A ) e. ( Base ` J ) /\ ( .1. .x. C ) e. ( Base ` J ) ) -> ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) e. ( Base ` J ) )
18	10 12 14 17	syl3anc	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) e. ( Base ` J ) )