Theorem rngqiprngfulem1

Description: Lemma 1 for rngqiprngfu (and lemma for rngqiprngu ). (Contributed by AV, 16-Mar-2025)

	Ref	Expression
Hypotheses	rngqiprngfu.r	|- ( ph -> R e. Rng )
	rngqiprngfu.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rngqiprngfu.j	|- J = ( R |`s I )
	rngqiprngfu.u	|- ( ph -> J e. Ring )
	rngqiprngfu.b	|- B = ( Base ` R )
	rngqiprngfu.t	|- .x. = ( .r ` R )
	rngqiprngfu.1	|- .1. = ( 1r ` J )
	rngqiprngfu.g	|- .~ = ( R ~QG I )
	rngqiprngfu.q	|- Q = ( R /s .~ )
	rngqiprngfu.v	|- ( ph -> Q e. Ring )
Assertion	rngqiprngfulem1	|- ( ph -> E. x e. B ( 1r ` Q ) = [ x ] .~ )

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	|- ( ph -> R e. Rng )
2		rngqiprngfu.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rngqiprngfu.j	|- J = ( R |`s I )
4		rngqiprngfu.u	|- ( ph -> J e. Ring )
5		rngqiprngfu.b	|- B = ( Base ` R )
6		rngqiprngfu.t	|- .x. = ( .r ` R )
7		rngqiprngfu.1	|- .1. = ( 1r ` J )
8		rngqiprngfu.g	|- .~ = ( R ~QG I )
9		rngqiprngfu.q	|- Q = ( R /s .~ )
10		rngqiprngfu.v	|- ( ph -> Q e. Ring )
11		eqid	|- ( Base ` Q ) = ( Base ` Q )
12		eqid	|- ( 1r ` Q ) = ( 1r ` Q )
13	11 12	ringidcl	|- ( Q e. Ring -> ( 1r ` Q ) e. ( Base ` Q ) )
14	10 13	syl	|- ( ph -> ( 1r ` Q ) e. ( Base ` Q ) )
15	9	a1i	|- ( ph -> Q = ( R /s .~ ) )
16	5	a1i	|- ( ph -> B = ( Base ` R ) )
17	8	ovexi	|- .~ e. _V
18	17	a1i	|- ( ph -> .~ e. _V )
19	15 16 18 1	qusbas	|- ( ph -> ( B /. .~ ) = ( Base ` Q ) )
20	14 19	eleqtrrd	|- ( ph -> ( 1r ` Q ) e. ( B /. .~ ) )
21		fvexd	|- ( ph -> ( 1r ` Q ) e. _V )
22		elqsg	|- ( ( 1r ` Q ) e. _V -> ( ( 1r ` Q ) e. ( B /. .~ ) <-> E. x e. B ( 1r ` Q ) = [ x ] .~ ) )
23	21 22	syl	|- ( ph -> ( ( 1r ` Q ) e. ( B /. .~ ) <-> E. x e. B ( 1r ` Q ) = [ x ] .~ ) )
24	20 23	mpbid	|- ( ph -> E. x e. B ( 1r ` Q ) = [ x ] .~ )