Theorem rngqiprngghmlem3

Description: Lemma 3 for rngqiprngghm . (Contributed by AV, 25-Feb-2025) (Proof shortened by AV, 24-Mar-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	rngqiprngghmlem3	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. ( A ( +g ` R ) C ) ) = ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) )

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	1 2 3 4 5 6 7	rngqiprng1elbas	|- ( ph -> .1. e. B )
9	8	anim1i	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. e. B /\ ( A e. B /\ C e. B ) ) )
10		3anass	|- ( ( .1. e. B /\ A e. B /\ C e. B ) <-> ( .1. e. B /\ ( A e. B /\ C e. B ) ) )
11	9 10	sylibr	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. e. B /\ A e. B /\ C e. B ) )
12		eqid	|- ( +g ` R ) = ( +g ` R )
13	5 12 6	rngdi	|- ( ( R e. Rng /\ ( .1. e. B /\ A e. B /\ C e. B ) ) -> ( .1. .x. ( A ( +g ` R ) C ) ) = ( ( .1. .x. A ) ( +g ` R ) ( .1. .x. C ) ) )
14	1 11 13	syl2an2r	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. ( A ( +g ` R ) C ) ) = ( ( .1. .x. A ) ( +g ` R ) ( .1. .x. C ) ) )
15	3 12	ressplusg	|- ( I e. ( 2Ideal ` R ) -> ( +g ` R ) = ( +g ` J ) )
16	2 15	syl	|- ( ph -> ( +g ` R ) = ( +g ` J ) )
17	16	oveqd	|- ( ph -> ( ( .1. .x. A ) ( +g ` R ) ( .1. .x. C ) ) = ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) )
18	17	adantr	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( ( .1. .x. A ) ( +g ` R ) ( .1. .x. C ) ) = ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) )
19	14 18	eqtrd	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( .1. .x. ( A ( +g ` R ) C ) ) = ( ( .1. .x. A ) ( +g ` J ) ( .1. .x. C ) ) )