Theorem isrng

Description: The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Hypotheses	isrng.b	$$⊢B={\mathrm{Base}}_R$$
	isrng.g	$$⊢G={\mathrm{mulGrp}}_R$$
	isrng.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	isrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	isrng	Could not format assertion : No typesetting found for |- ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isrng.b	$$⊢B={\mathrm{Base}}_R$$
2		isrng.g	$$⊢G={\mathrm{mulGrp}}_R$$
3		isrng.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		isrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		fveq2	$$⊢r=R\to {\mathrm{mulGrp}}_r={\mathrm{mulGrp}}_R$$
6	5 2	eqtr4di	$$⊢r=R\to {\mathrm{mulGrp}}_r=G$$
7	6	eleq1d	Could not format ( r = R -> ( ( mulGrp ` r ) e. Smgrp <-> G e. Smgrp ) ) : No typesetting found for |- ( r = R -> ( ( mulGrp ` r ) e. Smgrp <-> G e. Smgrp ) ) with typecode |-
8		fvexd	$$⊢r=R\to {\mathrm{Base}}_r\in \mathrm{V}$$
9		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
10	9 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
11		fvexd	$$⊢\left(r=R\wedge b=B\right)\to {+}_r\in \mathrm{V}$$
12		fveq2	$$⊢r=R\to {+}_r={+}_R$$
13	12	adantr	$$⊢\left(r=R\wedge b=B\right)\to {+}_r={+}_R$$
14	13 3	eqtr4di	$$⊢\left(r=R\wedge b=B\right)\to {+}_r=\underset{\dot{}}{+}$$
15		fvexd	$$⊢\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\to {\cdot }_r\in \mathrm{V}$$
16		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
17	16	adantr	$$⊢\left(r=R\wedge b=B\right)\to {\cdot }_r={\cdot }_R$$
18	17	adantr	$$⊢\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\to {\cdot }_r={\cdot }_R$$
19	18 4	eqtr4di	$$⊢\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\to {\cdot }_r=\underset{\dot{}}{·}$$
20		simpllr	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to b=B$$
21		simpr	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to t=\underset{\dot{}}{·}$$
22		eqidd	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to x=x$$
23		oveq	$$⊢p=\underset{\dot{}}{+}\to ypz=y\underset{\dot{}}{+}z$$
24	23	ad2antlr	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to ypz=y\underset{\dot{}}{+}z$$
25	21 22 24	oveq123d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to xt\left(ypz\right)=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)$$
26		simpr	$$⊢\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\to p=\underset{\dot{}}{+}$$
27	26	adantr	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to p=\underset{\dot{}}{+}$$
28		oveq	$$⊢t=\underset{\dot{}}{·}\to xty=x\underset{\dot{}}{·}y$$
29	28	adantl	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to xty=x\underset{\dot{}}{·}y$$
30		oveq	$$⊢t=\underset{\dot{}}{·}\to xtz=x\underset{\dot{}}{·}z$$
31	30	adantl	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to xtz=x\underset{\dot{}}{·}z$$
32	27 29 31	oveq123d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(xty\right)p\left(xtz\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
33	25 32	eqeq12d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\leftrightarrow x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\right)$$
34		oveq	$$⊢p=\underset{\dot{}}{+}\to xpy=x\underset{\dot{}}{+}y$$
35	34	ad2antlr	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to xpy=x\underset{\dot{}}{+}y$$
36		eqidd	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to z=z$$
37	21 35 36	oveq123d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(xpy\right)tz=\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z$$
38		oveq	$$⊢t=\underset{\dot{}}{·}\to ytz=y\underset{\dot{}}{·}z$$
39	38	adantl	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to ytz=y\underset{\dot{}}{·}z$$
40	27 31 39	oveq123d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(xtz\right)p\left(ytz\right)=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
41	37 40	eqeq12d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(\left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\leftrightarrow \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)$$
42	33 41	anbi12d	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
43	20 42	raleqbidv	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
44	20 43	raleqbidv	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
45	20 44	raleqbidv	$$⊢\left(\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\wedge t=\underset{\dot{}}{·}\right)\to \left(\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
46	15 19 45	sbcied2	$$⊢\left(\left(r=R\wedge b=B\right)\wedge p=\underset{\dot{}}{+}\right)\to \left(\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
47	11 14 46	sbcied2	$$⊢\left(r=R\wedge b=B\right)\to \left(\underset{\dot{}}{[}{+}_r/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
48	8 10 47	sbcied2	$$⊢r=R\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_r/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_r/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xt\left(ypz\right)=\left(xty\right)p\left(xtz\right)\wedge \left(xpy\right)tz=\left(xtz\right)p\left(ytz\right)\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\wedge \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)$$
49	7 48	anbi12d	Could not format ( r = R -> ( ( ( mulGrp ` r ) e. Smgrp /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) <-> ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) ) : No typesetting found for |- ( r = R -> ( ( ( mulGrp ` r ) e. Smgrp /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) <-> ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) ) with typecode |-
50		df-rng0	Could not format Rng = { r e. Abel | ( ( mulGrp ` r ) e. Smgrp /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) } : No typesetting found for |- Rng = { r e. Abel | ( ( mulGrp ` r ) e. Smgrp /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) } with typecode |-
51	49 50	elrab2	Could not format ( R e. Rng <-> ( R e. Abel /\ ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) ) : No typesetting found for |- ( R e. Rng <-> ( R e. Abel /\ ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) ) with typecode |-
52		3anass	Could not format ( ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> ( R e. Abel /\ ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) ) : No typesetting found for |- ( ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> ( R e. Abel /\ ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) ) with typecode |-
53	51 52	bitr4i	Could not format ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) : No typesetting found for |- ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) with typecode |-