Theorem rngqiprngfulem3

Description: Lemma 3 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 )
	rngqiprngfu.e	|- ( ph -> E e. ( 1r ` Q ) )
	rngqiprngfu.m	|- .- = ( -g ` R )
	rngqiprngfu.a	|- .+ = ( +g ` R )
	rngqiprngfu.n	|- U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
Assertion	rngqiprngfulem3	|- ( ph -> U e. B )

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		rngqiprngfu.e	|- ( ph -> E e. ( 1r ` Q ) )
12		rngqiprngfu.m	|- .- = ( -g ` R )
13		rngqiprngfu.a	|- .+ = ( +g ` R )
14		rngqiprngfu.n	|- U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
15		rnggrp	|- ( R e. Rng -> R e. Grp )
16	1 15	syl	|- ( ph -> R e. Grp )
17	1 2 3 4 5 6 7 8 9 10 11	rngqiprngfulem2	|- ( ph -> E e. B )
18	1 2 3 4 5 6 7	rngqiprng1elbas	|- ( ph -> .1. e. B )
19	5 6	rngcl	|- ( ( R e. Rng /\ .1. e. B /\ E e. B ) -> ( .1. .x. E ) e. B )
20	1 18 17 19	syl3anc	|- ( ph -> ( .1. .x. E ) e. B )
21	5 12	grpsubcl	|- ( ( R e. Grp /\ E e. B /\ ( .1. .x. E ) e. B ) -> ( E .- ( .1. .x. E ) ) e. B )
22	16 17 20 21	syl3anc	|- ( ph -> ( E .- ( .1. .x. E ) ) e. B )
23	5 13 16 22 18	grpcld	|- ( ph -> ( ( E .- ( .1. .x. E ) ) .+ .1. ) e. B )
24	14 23	eqeltrid	|- ( ph -> U e. B )