Theorem fracfld

Description: The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypothesis	fracfld.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
Assertion	fracfld	Could not format assertion : No typesetting found for |- ( ph -> ( Frac ` R ) e. Field ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fracfld.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
2		fracval	Could not format ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) with typecode |-
3	1	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
4		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
5		eqid	$$⊢1_R=1_R$$
6		eqid	$$⊢0_R=0_R$$
7	5 6	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
8	3 4 7	3syl	$$⊢\phi \to 1_R\ne 0_R$$
9		fvex	$$⊢1_R\in \mathrm{V}$$
10	9 9	op1st	$$⊢1^{st}\left(⟨1_R,1_R⟩\right)=1_R$$
11	10	a1i	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) = ( 1r ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) = ( 1r ` R ) ) with typecode |-
12		fvex	$$⊢0_R\in \mathrm{V}$$
13	12 9	op2nd	$$⊢2^{nd}\left(⟨0_R,1_R⟩\right)=1_R$$
14	13	a1i	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) = ( 1r ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) = ( 1r ` R ) ) with typecode |-
15	11 14	oveq12d	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) = ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) = ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) ) with typecode |-
16		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
17		eqid	$$⊢{\cdot }_R={\cdot }_R$$
18	1	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
19	18	ad2antrr	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> R e. Ring ) with typecode |-
20	16 5	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
21	19 20	syl	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) ) with typecode |-
22	16 17 5 19 21	ringlidmd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) ) with typecode |-
23	15 22	eqtrd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) = ( 1r ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) = ( 1r ` R ) ) with typecode |-
24	12 9	op1st	$$⊢1^{st}\left(⟨0_R,1_R⟩\right)=0_R$$
25	24	a1i	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) = ( 0g ` R ) ) with typecode |-
26	9 9	op2nd	$$⊢2^{nd}\left(⟨1_R,1_R⟩\right)=1_R$$
27	26	a1i	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) = ( 1r ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) = ( 1r ` R ) ) with typecode |-
28	25 27	oveq12d	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) = ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) = ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) ) with typecode |-
29	18	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
30	16 6	grpidcl	$$⊢R\in \mathrm{Grp}\to 0_R\in {\mathrm{Base}}_R$$
31	29 30	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
32	31	ad2antrr	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) ) with typecode |-
33	16 17 5 19 32	ringridmd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) with typecode |-
34	28 33	eqtrd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) = ( 0g ` R ) ) with typecode |-
35	23 34	oveq12d	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) = ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) = ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) ) with typecode |-
36	35	oveq2d	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( t ( .r ` R ) ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( t ( .r ` R ) ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) ) ) with typecode |-
37		eqid	$$⊢{-}_R={-}_R$$
38		eqid	$$⊢\mathrm{RLReg}\left(R\right)=\mathrm{RLReg}\left(R\right)$$
39	38 16	rrgss	$$⊢\mathrm{RLReg}\left(R\right)\subseteq {\mathrm{Base}}_R$$
40	39	a1i	Could not format ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( RLReg ` R ) C_ ( Base ` R ) ) : No typesetting found for |- ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( RLReg ` R ) C_ ( Base ` R ) ) with typecode |-
41	40	sselda	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> t e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> t e. ( Base ` R ) ) with typecode |-
42	16 17 37 19 41 21 32	ringsubdi	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) ) = ( ( t ( .r ` R ) ( 1r ` R ) ) ( -g ` R ) ( t ( .r ` R ) ( 0g ` R ) ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) ) = ( ( t ( .r ` R ) ( 1r ` R ) ) ( -g ` R ) ( t ( .r ` R ) ( 0g ` R ) ) ) ) with typecode |-
43	16 17 5 19 41	ringridmd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( 1r ` R ) ) = t ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( 1r ` R ) ) = t ) with typecode |-
44	16 17 6 19 41	ringrzd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) with typecode |-
45	43 44	oveq12d	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( t ( .r ` R ) ( 1r ` R ) ) ( -g ` R ) ( t ( .r ` R ) ( 0g ` R ) ) ) = ( t ( -g ` R ) ( 0g ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( t ( .r ` R ) ( 1r ` R ) ) ( -g ` R ) ( t ( .r ` R ) ( 0g ` R ) ) ) = ( t ( -g ` R ) ( 0g ` R ) ) ) with typecode |-
46	29	ad2antrr	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> R e. Grp ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> R e. Grp ) with typecode |-
47	16 6 37	grpsubid1	$$⊢\left(R\in \mathrm{Grp}\wedge t\in {\mathrm{Base}}_R\right)\to t{-}_R{0}_R=t$$
48	46 41 47	syl2anc	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( -g ` R ) ( 0g ` R ) ) = t ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( -g ` R ) ( 0g ` R ) ) = t ) with typecode |-
49	45 48	eqtrd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( t ( .r ` R ) ( 1r ` R ) ) ( -g ` R ) ( t ( .r ` R ) ( 0g ` R ) ) ) = t ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( t ( .r ` R ) ( 1r ` R ) ) ( -g ` R ) ( t ( .r ` R ) ( 0g ` R ) ) ) = t ) with typecode |-
50	36 42 49	3eqtrd	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = t ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = t ) with typecode |-
51	50	eqeq1d	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) <-> t = ( 0g ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> ( ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) <-> t = ( 0g ` R ) ) ) with typecode |-
52	51	biimpa	Could not format ( ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) /\ ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) -> t = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) /\ ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) -> t = ( 0g ` R ) ) with typecode |-
53		simpr	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> t e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> t e. ( RLReg ` R ) ) with typecode |-
54	38 6	rrgnz	$$⊢R\in \mathrm{NzRing}\to \neg 0_R\in \mathrm{RLReg}\left(R\right)$$
55	3 4 54	3syl	$$⊢\phi \to \neg 0_R\in \mathrm{RLReg}\left(R\right)$$
56	55	ad2antrr	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> -. ( 0g ` R ) e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> -. ( 0g ` R ) e. ( RLReg ` R ) ) with typecode |-
57		nelne2	$$⊢\left(t\in \mathrm{RLReg}\left(R\right)\wedge \neg 0_R\in \mathrm{RLReg}\left(R\right)\right)\to t\ne 0_R$$
58	53 56 57	syl2anc	Could not format ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> t =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) -> t =/= ( 0g ` R ) ) with typecode |-
59	58	adantr	Could not format ( ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) /\ ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) -> t =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) /\ ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) -> t =/= ( 0g ` R ) ) with typecode |-
60	52 59	pm2.21ddne	Could not format ( ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) /\ ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) -> ( 1r ` R ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) /\ t e. ( RLReg ` R ) ) /\ ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) -> ( 1r ` R ) = ( 0g ` R ) ) with typecode |-
61		eqid	Could not format ( R ~RL ( RLReg ` R ) ) = ( R ~RL ( RLReg ` R ) ) : No typesetting found for |- ( R ~RL ( RLReg ` R ) ) = ( R ~RL ( RLReg ` R ) ) with typecode |-
62		eqid	$$⊢{\mathrm{Base}}_R\times \mathrm{RLReg}\left(R\right)={\mathrm{Base}}_R\times \mathrm{RLReg}\left(R\right)$$
63	1	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
64	16 38 6	isdomn6	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge {\mathrm{Base}}_R\setminus \left\{0_R\right\}=\mathrm{RLReg}\left(R\right)\right)$$
65	3 64	sylib	$$⊢\phi \to \left(R\in \mathrm{NzRing}\wedge {\mathrm{Base}}_R\setminus \left\{0_R\right\}=\mathrm{RLReg}\left(R\right)\right)$$
66	65	simprd	$$⊢\phi \to {\mathrm{Base}}_R\setminus \left\{0_R\right\}=\mathrm{RLReg}\left(R\right)$$
67		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
68	16 6 67	isdomn3	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{Ring}\wedge {\mathrm{Base}}_R\setminus \left\{0_R\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\right)$$
69	3 68	sylib	$$⊢\phi \to \left(R\in \mathrm{Ring}\wedge {\mathrm{Base}}_R\setminus \left\{0_R\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\right)$$
70	69	simprd	$$⊢\phi \to {\mathrm{Base}}_R\setminus \left\{0_R\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
71	66 70	eqeltrrd	$$⊢\phi \to \mathrm{RLReg}\left(R\right)\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
72	16 6 5 17 37 62 61 63 71	erler	Could not format ( ph -> ( R ~RL ( RLReg ` R ) ) Er ( ( Base ` R ) X. ( RLReg ` R ) ) ) : No typesetting found for |- ( ph -> ( R ~RL ( RLReg ` R ) ) Er ( ( Base ` R ) X. ( RLReg ` R ) ) ) with typecode |-
73	18 20	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
74	5 38 18	1rrg	$$⊢\phi \to 1_R\in \mathrm{RLReg}\left(R\right)$$
75	73 74	opelxpd	$$⊢\phi \to ⟨1_R,1_R⟩\in \left({\mathrm{Base}}_R\times \mathrm{RLReg}\left(R\right)\right)$$
76	72 75	erth	Could not format ( ph -> ( <. ( 1r ` R ) , ( 1r ` R ) >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. <-> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ( <. ( 1r ` R ) , ( 1r ` R ) >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. <-> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
77	76	biimpar	Could not format ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> <. ( 1r ` R ) , ( 1r ` R ) >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. ) : No typesetting found for |- ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> <. ( 1r ` R ) , ( 1r ` R ) >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. ) with typecode |-
78	16 61 40 6 17 37 77	erldi	Could not format ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> E. t e. ( RLReg ` R ) ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> E. t e. ( RLReg ` R ) ( t ( .r ` R ) ( ( ( 1st ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ) ( -g ` R ) ( ( 1st ` <. ( 0g ` R ) , ( 1r ` R ) >. ) ( .r ` R ) ( 2nd ` <. ( 1r ` R ) , ( 1r ` R ) >. ) ) ) ) = ( 0g ` R ) ) with typecode |-
79	60 78	r19.29a	Could not format ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( 1r ` R ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ph /\ [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( 1r ` R ) = ( 0g ` R ) ) with typecode |-
80	8 79	mteqand	Could not format ( ph -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) =/= [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ph -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) =/= [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
81		eqid	Could not format ( R RLocal ( RLReg ` R ) ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( R RLocal ( RLReg ` R ) ) = ( R RLocal ( RLReg ` R ) ) with typecode |-
82		eqid	Could not format [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) : No typesetting found for |- [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) with typecode |-
83	6 5 81 61 63 71 82	rloc1r	Could not format ( ph -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
84		eqid	Could not format [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) : No typesetting found for |- [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) with typecode |-
85	6 5 81 61 63 71 84	rloc0g	Could not format ( ph -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
86	80 83 85	3netr3d	Could not format ( ph -> ( 1r ` ( R RLocal ( RLReg ` R ) ) ) =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ( 1r ` ( R RLocal ( RLReg ` R ) ) ) =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
87		oveq2	Could not format ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
88	87	eqeq1d	Could not format ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) <-> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) <-> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) with typecode |-
89		oveq1	Could not format ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) ) : No typesetting found for |- ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) ) with typecode |-
90	89	eqeq1d	Could not format ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) <-> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) <-> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) with typecode |-
91	88 90	anbi12d	Could not format ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) <-> ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( y = [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) -> ( ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) <-> ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) ) with typecode |-
92		simplr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> b e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> b e. ( RLReg ` R ) ) with typecode |-
93	39 92	sselid	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> b e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> b e. ( Base ` R ) ) with typecode |-
94		simpllr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a e. ( Base ` R ) ) with typecode |-
95		simplr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
96	72	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( R ~RL ( RLReg ` R ) ) Er ( ( Base ` R ) X. ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( R ~RL ( RLReg ` R ) ) Er ( ( Base ` R ) X. ( RLReg ` R ) ) ) with typecode |-
97	18	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> R e. Ring ) with typecode |-
98	97 20	syl	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) ) with typecode |-
99	16 17 6 97 98	ringlzd	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 0g ` R ) ) with typecode |-
100		simpr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> a = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> a = ( 0g ` R ) ) with typecode |-
101	100	oveq1d	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( a ( .r ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( a ( .r ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( .r ` R ) ( 1r ` R ) ) ) with typecode |-
102	93	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> b e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> b e. ( Base ` R ) ) with typecode |-
103	16 17 6 97 102	ringlzd	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) b ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) b ) = ( 0g ` R ) ) with typecode |-
104	99 101 103	3eqtr4d	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( a ( .r ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( .r ` R ) b ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( a ( .r ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( .r ` R ) b ) ) with typecode |-
105	63	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> R e. CRing ) with typecode |-
106	94	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> a e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> a e. ( Base ` R ) ) with typecode |-
107	31	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) ) with typecode |-
108	92	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> b e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> b e. ( RLReg ` R ) ) with typecode |-
109	74	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( 1r ` R ) e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( 1r ` R ) e. ( RLReg ` R ) ) with typecode |-
110	16 17 61 105 106 107 108 109	fracerl	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( <. a , b >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. <-> ( a ( .r ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( .r ` R ) b ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> ( <. a , b >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. <-> ( a ( .r ` R ) ( 1r ` R ) ) = ( ( 0g ` R ) ( .r ` R ) b ) ) ) with typecode |-
111	104 110	mpbird	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> <. a , b >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> <. a , b >. ( R ~RL ( RLReg ` R ) ) <. ( 0g ` R ) , ( 1r ` R ) >. ) with typecode |-
112	96 111	erthi	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
113	85	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
114	95 112 113	3eqtrd	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> x = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> x = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
115		eldifsni	Could not format ( x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) -> x =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) -> x =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
116	115	ad5antlr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> x =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> x =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
117	116	neneqd	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> -. x = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ a = ( 0g ` R ) ) -> -. x = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
118	114 117	pm2.65da	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> -. a = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> -. a = ( 0g ` R ) ) with typecode |-
119	118	neqned	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a =/= ( 0g ` R ) ) with typecode |-
120	94 119	eldifsnd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) with typecode |-
121	66	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( Base ` R ) \ { ( 0g ` R ) } ) = ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( Base ` R ) \ { ( 0g ` R ) } ) = ( RLReg ` R ) ) with typecode |-
122	120 121	eleqtrd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> a e. ( RLReg ` R ) ) with typecode |-
123	93 122	opelxpd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> <. b , a >. e. ( ( Base ` R ) X. ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> <. b , a >. e. ( ( Base ` R ) X. ( RLReg ` R ) ) ) with typecode |-
124		ovex	Could not format ( R ~RL ( RLReg ` R ) ) e. _V : No typesetting found for |- ( R ~RL ( RLReg ` R ) ) e. _V with typecode |-
125	124	ecelqsi	Could not format ( <. b , a >. e. ( ( Base ` R ) X. ( RLReg ` R ) ) -> [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) e. ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( <. b , a >. e. ( ( Base ` R ) X. ( RLReg ` R ) ) -> [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) e. ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
126	123 125	syl	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) e. ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) e. ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
127	39	a1i	$$⊢\phi \to \mathrm{RLReg}\left(R\right)\subseteq {\mathrm{Base}}_R$$
128	16 6 17 37 62 81 61 1 127	rlocbas	Could not format ( ph -> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
129	128	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
130	126 129	eleqtrd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
131		eqid	Could not format ( Base ` ( R RLocal ( RLReg ` R ) ) ) = ( Base ` ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( Base ` ( R RLocal ( RLReg ` R ) ) ) = ( Base ` ( R RLocal ( RLReg ` R ) ) ) with typecode |-
132		eqid	Could not format ( .r ` ( R RLocal ( RLReg ` R ) ) ) = ( .r ` ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( .r ` ( R RLocal ( RLReg ` R ) ) ) = ( .r ` ( R RLocal ( RLReg ` R ) ) ) with typecode |-
133		eqid	$$⊢{+}_R={+}_R$$
134	16 17 133 81 61 63 71	rloccring	Could not format ( ph -> ( R RLocal ( RLReg ` R ) ) e. CRing ) : No typesetting found for |- ( ph -> ( R RLocal ( RLReg ` R ) ) e. CRing ) with typecode |-
135	134	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( R RLocal ( RLReg ` R ) ) e. CRing ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( R RLocal ( RLReg ` R ) ) e. CRing ) with typecode |-
136		simp-4r	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) with typecode |-
137	136	eldifad	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> x e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> x e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
138	131 132 135 137 130	crngcomd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) ) with typecode |-
139		simpr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
140	139	oveq2d	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
141	63	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> R e. CRing ) with typecode |-
142	71	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( RLReg ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( RLReg ` R ) e. ( SubMnd ` ( mulGrp ` R ) ) ) with typecode |-
143	16 17 133 81 61 141 142 93 94 122 92 132	rlocmulval	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) = [ <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) = [ <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
144	72	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( R ~RL ( RLReg ` R ) ) Er ( ( Base ` R ) X. ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( R ~RL ( RLReg ` R ) ) Er ( ( Base ` R ) X. ( RLReg ` R ) ) ) with typecode |-
145	16 17 141 93 94	crngcomd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( b ( .r ` R ) a ) = ( a ( .r ` R ) b ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( b ( .r ` R ) a ) = ( a ( .r ` R ) b ) ) with typecode |-
146	18	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> R e. Ring ) with typecode |-
147	16 17 146 93 94	ringcld	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( b ( .r ` R ) a ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( b ( .r ` R ) a ) e. ( Base ` R ) ) with typecode |-
148	16 17 5 146 147	ringridmd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( b ( .r ` R ) a ) ( .r ` R ) ( 1r ` R ) ) = ( b ( .r ` R ) a ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( b ( .r ` R ) a ) ( .r ` R ) ( 1r ` R ) ) = ( b ( .r ` R ) a ) ) with typecode |-
149	16 17 146 94 93	ringcld	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) e. ( Base ` R ) ) with typecode |-
150	16 17 5 146 149	ringlidmd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( 1r ` R ) ( .r ` R ) ( a ( .r ` R ) b ) ) = ( a ( .r ` R ) b ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( 1r ` R ) ( .r ` R ) ( a ( .r ` R ) b ) ) = ( a ( .r ` R ) b ) ) with typecode |-
151	145 148 150	3eqtr4d	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( b ( .r ` R ) a ) ( .r ` R ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) ( a ( .r ` R ) b ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( b ( .r ` R ) a ) ( .r ` R ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) ( a ( .r ` R ) b ) ) ) with typecode |-
152	73	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( 1r ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( 1r ` R ) e. ( Base ` R ) ) with typecode |-
153	92	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> b e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> b e. ( RLReg ` R ) ) with typecode |-
154	66	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( ( Base ` R ) \ { ( 0g ` R ) } ) = ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( ( Base ` R ) \ { ( 0g ` R ) } ) = ( RLReg ` R ) ) with typecode |-
155	153 154	eleqtrrd	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> b e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> b e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) with typecode |-
156	94	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> a e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> a e. ( Base ` R ) ) with typecode |-
157	31	ad5antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( 0g ` R ) e. ( Base ` R ) ) with typecode |-
158	1	adantr	Could not format ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> R e. IDomn ) : No typesetting found for |- ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> R e. IDomn ) with typecode |-
159	158	ad4antr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> R e. IDomn ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> R e. IDomn ) with typecode |-
160		simpr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( a ( .r ` R ) b ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( a ( .r ` R ) b ) = ( 0g ` R ) ) with typecode |-
161	146	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> R e. Ring ) with typecode |-
162	93	adantr	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> b e. ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> b e. ( Base ` R ) ) with typecode |-
163	16 17 6 161 162	ringlzd	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) b ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) b ) = ( 0g ` R ) ) with typecode |-
164	160 163	eqtr4d	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( a ( .r ` R ) b ) = ( ( 0g ` R ) ( .r ` R ) b ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> ( a ( .r ` R ) b ) = ( ( 0g ` R ) ( .r ` R ) b ) ) with typecode |-
165	16 6 17 155 156 157 159 164	idomrcan	Could not format ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> a = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) /\ ( a ( .r ` R ) b ) = ( 0g ` R ) ) -> a = ( 0g ` R ) ) with typecode |-
166	118 165	mtand	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> -. ( a ( .r ` R ) b ) = ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> -. ( a ( .r ` R ) b ) = ( 0g ` R ) ) with typecode |-
167	166	neqned	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) =/= ( 0g ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) =/= ( 0g ` R ) ) with typecode |-
168	149 167	eldifsnd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) with typecode |-
169	168 121	eleqtrd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( a ( .r ` R ) b ) e. ( RLReg ` R ) ) with typecode |-
170	74	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( 1r ` R ) e. ( RLReg ` R ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( 1r ` R ) e. ( RLReg ` R ) ) with typecode |-
171	16 17 61 141 147 152 169 170	fracerl	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ( R ~RL ( RLReg ` R ) ) <. ( 1r ` R ) , ( 1r ` R ) >. <-> ( ( b ( .r ` R ) a ) ( .r ` R ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) ( a ( .r ` R ) b ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ( R ~RL ( RLReg ` R ) ) <. ( 1r ` R ) , ( 1r ` R ) >. <-> ( ( b ( .r ` R ) a ) ( .r ` R ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) ( a ( .r ` R ) b ) ) ) ) with typecode |-
172	151 171	mpbird	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ( R ~RL ( RLReg ` R ) ) <. ( 1r ` R ) , ( 1r ` R ) >. ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ( R ~RL ( RLReg ` R ) ) <. ( 1r ` R ) , ( 1r ` R ) >. ) with typecode |-
173	144 172	erthi	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. ( b ( .r ` R ) a ) , ( a ( .r ` R ) b ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
174	143 173	eqtrd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
175	83	ad4antr	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
176	140 174 175	3eqtrd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
177	138 176	eqtrd	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) with typecode |-
178	177 176	jca	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( [ <. b , a >. ] ( R ~RL ( RLReg ` R ) ) ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) with typecode |-
179	91 130 178	rspcedvdw	Could not format ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) /\ a e. ( Base ` R ) ) /\ b e. ( RLReg ` R ) ) /\ x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) -> E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) with typecode |-
180	128	difeq1d	Could not format ( ph -> ( ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) = ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) : No typesetting found for |- ( ph -> ( ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) = ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) with typecode |-
181	180	eleq2d	Could not format ( ph -> ( x e. ( ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) <-> x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) ) : No typesetting found for |- ( ph -> ( x e. ( ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) <-> x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) ) with typecode |-
182	181	biimpar	Could not format ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> x e. ( ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) : No typesetting found for |- ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> x e. ( ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) with typecode |-
183	182	eldifad	Could not format ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> x e. ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> x e. ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
184	183	elrlocbasi	Could not format ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> E. a e. ( Base ` R ) E. b e. ( RLReg ` R ) x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> E. a e. ( Base ` R ) E. b e. ( RLReg ` R ) x = [ <. a , b >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
185	179 184	r19.29vva	Could not format ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) ) -> E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) with typecode |-
186	185	ralrimiva	Could not format ( ph -> A. x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( ph -> A. x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) with typecode |-
187		eqid	Could not format ( 0g ` ( R RLocal ( RLReg ` R ) ) ) = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( 0g ` ( R RLocal ( RLReg ` R ) ) ) = ( 0g ` ( R RLocal ( RLReg ` R ) ) ) with typecode |-
188		eqid	Could not format ( 1r ` ( R RLocal ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( 1r ` ( R RLocal ( RLReg ` R ) ) ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) with typecode |-
189		eqid	Could not format ( Unit ` ( R RLocal ( RLReg ` R ) ) ) = ( Unit ` ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( Unit ` ( R RLocal ( RLReg ` R ) ) ) = ( Unit ` ( R RLocal ( RLReg ` R ) ) ) with typecode |-
190	134	crngringd	Could not format ( ph -> ( R RLocal ( RLReg ` R ) ) e. Ring ) : No typesetting found for |- ( ph -> ( R RLocal ( RLReg ` R ) ) e. Ring ) with typecode |-
191	131 187 188 132 189 190	isdrng4	Could not format ( ph -> ( ( R RLocal ( RLReg ` R ) ) e. DivRing <-> ( ( 1r ` ( R RLocal ( RLReg ` R ) ) ) =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) /\ A. x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( R RLocal ( RLReg ` R ) ) e. DivRing <-> ( ( 1r ` ( R RLocal ( RLReg ` R ) ) ) =/= ( 0g ` ( R RLocal ( RLReg ` R ) ) ) /\ A. x e. ( ( Base ` ( R RLocal ( RLReg ` R ) ) ) \ { ( 0g ` ( R RLocal ( RLReg ` R ) ) ) } ) E. y e. ( Base ` ( R RLocal ( RLReg ` R ) ) ) ( ( x ( .r ` ( R RLocal ( RLReg ` R ) ) ) y ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) /\ ( y ( .r ` ( R RLocal ( RLReg ` R ) ) ) x ) = ( 1r ` ( R RLocal ( RLReg ` R ) ) ) ) ) ) ) with typecode |-
192	86 186 191	mpbir2and	Could not format ( ph -> ( R RLocal ( RLReg ` R ) ) e. DivRing ) : No typesetting found for |- ( ph -> ( R RLocal ( RLReg ` R ) ) e. DivRing ) with typecode |-
193		isfld	Could not format ( ( R RLocal ( RLReg ` R ) ) e. Field <-> ( ( R RLocal ( RLReg ` R ) ) e. DivRing /\ ( R RLocal ( RLReg ` R ) ) e. CRing ) ) : No typesetting found for |- ( ( R RLocal ( RLReg ` R ) ) e. Field <-> ( ( R RLocal ( RLReg ` R ) ) e. DivRing /\ ( R RLocal ( RLReg ` R ) ) e. CRing ) ) with typecode |-
194	192 134 193	sylanbrc	Could not format ( ph -> ( R RLocal ( RLReg ` R ) ) e. Field ) : No typesetting found for |- ( ph -> ( R RLocal ( RLReg ` R ) ) e. Field ) with typecode |-
195	2 194	eqeltrid	Could not format ( ph -> ( Frac ` R ) e. Field ) : No typesetting found for |- ( ph -> ( Frac ` R ) e. Field ) with typecode |-