Theorem rngqiprnglinlem3

Description: Lemma 3 for rngqiprnglin . (Contributed by AV, 28-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 )
	rngqiprngim.g	|- .~ = ( R ~QG I )
	rngqiprngim.q	|- Q = ( R /s .~ )
Assertion	rngqiprnglinlem3	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) e. ( Base ` Q ) )

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		rngqiprngim.g	|- .~ = ( R ~QG I )
9		rngqiprngim.q	|- Q = ( R /s .~ )
10	1 2 3 4 5 6 7 8 9	rngqiprnglinlem2	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A .x. C ) ] .~ = ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) )
11	1	anim1i	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( R e. Rng /\ ( A e. B /\ C e. B ) ) )
12		3anass	|- ( ( R e. Rng /\ A e. B /\ C e. B ) <-> ( R e. Rng /\ ( A e. B /\ C e. B ) ) )
13	11 12	sylibr	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( R e. Rng /\ A e. B /\ C e. B ) )
14	5 6	rngcl	|- ( ( R e. Rng /\ A e. B /\ C e. B ) -> ( A .x. C ) e. B )
15	13 14	syl	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( A .x. C ) e. B )
16		eqid	|- ( Base ` Q ) = ( Base ` Q )
17	8 9 5 16	quseccl0	|- ( ( R e. Rng /\ ( A .x. C ) e. B ) -> [ ( A .x. C ) ] .~ e. ( Base ` Q ) )
18	1 15 17	syl2an2r	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A .x. C ) ] .~ e. ( Base ` Q ) )
19	10 18	eqeltrrd	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( .r ` Q ) [ C ] .~ ) e. ( Base ` Q ) )