Theorem rngohomco

Description: The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Assertion	rngohomco	Could not format assertion : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢1^{st}\left(S\right)=1^{st}\left(S\right)$$
2		eqid	$$⊢\mathrm{ran}{1}^{st}\left(S\right)=\mathrm{ran}{1}^{st}\left(S\right)$$
3		eqid	$$⊢1^{st}\left(T\right)=1^{st}\left(T\right)$$
4		eqid	$$⊢\mathrm{ran}{1}^{st}\left(T\right)=\mathrm{ran}{1}^{st}\left(T\right)$$
5	1 2 3 4	rngohomf	Could not format ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) : No typesetting found for |- ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) with typecode |-
6	5	3expa	Could not format ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) with typecode |-
7	6	3adantl1	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) with typecode |-
8	7	adantrl	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) ) with typecode |-
9		eqid	$$⊢1^{st}\left(R\right)=1^{st}\left(R\right)$$
10		eqid	$$⊢\mathrm{ran}{1}^{st}\left(R\right)=\mathrm{ran}{1}^{st}\left(R\right)$$
11	9 10 1 2	rngohomf	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) with typecode |-
12	11	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) with typecode |-
13	12	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) with typecode |-
14	13	adantrr	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) with typecode |-
15		fco	$$⊢\left(G:\mathrm{ran}{1}^{st}\left(S\right)⟶\mathrm{ran}{1}^{st}\left(T\right)\wedge F:\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(S\right)\right)\to \left(G\circ F\right):\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(T\right)$$
16	8 14 15	syl2anc	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) ) with typecode |-
17		eqid	$$⊢2^{nd}\left(R\right)=2^{nd}\left(R\right)$$
18		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(R\right)\right)=\mathrm{GId}\left(2^{nd}\left(R\right)\right)$$
19	10 17 18	rngo1cl	$$⊢R\in \mathrm{RingOps}\to \mathrm{GId}\left(2^{nd}\left(R\right)\right)\in \mathrm{ran}{1}^{st}\left(R\right)$$
20	19	3ad2ant1	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge T\in \mathrm{RingOps}\right)\to \mathrm{GId}\left(2^{nd}\left(R\right)\right)\in \mathrm{ran}{1}^{st}\left(R\right)$$
21	20	adantr	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) ) with typecode |-
22		fvco3	$$⊢\left(F:\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(S\right)\wedge \mathrm{GId}\left(2^{nd}\left(R\right)\right)\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to \left(G\circ F\right)\left(\mathrm{GId}\left(2^{nd}\left(R\right)\right)\right)=G\left(F\left(\mathrm{GId}\left(2^{nd}\left(R\right)\right)\right)\right)$$
23	14 21 22	syl2anc	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) ) with typecode |-
24		eqid	$$⊢2^{nd}\left(S\right)=2^{nd}\left(S\right)$$
25		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(S\right)\right)=\mathrm{GId}\left(2^{nd}\left(S\right)\right)$$
26	17 18 24 25	rngohom1	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) with typecode |-
27	26	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) with typecode |-
28	27	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) with typecode |-
29	28	adantrr	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) ) with typecode |-
30	29	fveq2d	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) = ( G ` ( GId ` ( 2nd ` S ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) = ( G ` ( GId ` ( 2nd ` S ) ) ) ) with typecode |-
31		eqid	$$⊢2^{nd}\left(T\right)=2^{nd}\left(T\right)$$
32		eqid	$$⊢\mathrm{GId}\left(2^{nd}\left(T\right)\right)=\mathrm{GId}\left(2^{nd}\left(T\right)\right)$$
33	24 25 31 32	rngohom1	Could not format ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) : No typesetting found for |- ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) with typecode |-
34	33	3expa	Could not format ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) with typecode |-
35	34	3adantl1	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) with typecode |-
36	35	adantrl	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) ) with typecode |-
37	30 36	eqtrd	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) = ( GId ` ( 2nd ` T ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) = ( GId ` ( 2nd ` T ) ) ) with typecode |-
38	23 37	eqtrd	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) ) with typecode |-
39	9 10 1	rngohomadd	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) with typecode |-
40	39	ex	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) with typecode |-
41	40	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) with typecode |-
42	41	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) with typecode |-
43	42	imp	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) with typecode |-
44	43	adantlrr	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) with typecode |-
45	44	fveq2d	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) = ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) = ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) ) with typecode |-
46	9 10 1 2	rngohomcl	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ x e. ran ( 1st ` R ) ) -> ( F ` x ) e. ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ x e. ran ( 1st ` R ) ) -> ( F ` x ) e. ran ( 1st ` S ) ) with typecode |-
47	9 10 1 2	rngohomcl	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ y e. ran ( 1st ` R ) ) -> ( F ` y ) e. ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ y e. ran ( 1st ` R ) ) -> ( F ` y ) e. ran ( 1st ` S ) ) with typecode |-
48	46 47	anim12dan	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) with typecode |-
49	48	ex	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) ) with typecode |-
50	49	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) ) with typecode |-
51	50	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) ) with typecode |-
52	51	imp	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) with typecode |-
53	52	adantlrr	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) with typecode |-
54	1 2 3	rngohomadd	Could not format ( ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
55	54	ex	Could not format ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) ) with typecode |-
56	55	3expa	Could not format ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) ) with typecode |-
57	56	3adantl1	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) ) with typecode |-
58	57	imp	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
59	58	adantlrl	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
60	53 59	syldan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
61	45 60	eqtrd	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
62	9 10	rngogcl	$$⊢\left(R\in \mathrm{RingOps}\wedge x\in \mathrm{ran}{1}^{st}\left(R\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to x{1}^{st}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)$$
63	62	3expb	$$⊢\left(R\in \mathrm{RingOps}\wedge \left(x\in \mathrm{ran}{1}^{st}\left(R\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\right)\to x{1}^{st}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)$$
64	63	3ad2antl1	$$⊢\left(\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge T\in \mathrm{RingOps}\right)\wedge \left(x\in \mathrm{ran}{1}^{st}\left(R\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\right)\to x{1}^{st}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)$$
65	64	adantlr	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) ) with typecode |-
66		fvco3	$$⊢\left(F:\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(S\right)\wedge x{1}^{st}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to \left(G\circ F\right)\left(x{1}^{st}\left(R\right)y\right)=G\left(F\left(x{1}^{st}\left(R\right)y\right)\right)$$
67	14 66	sylan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) ) with typecode |-
68	65 67	syldan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) ) with typecode |-
69		fvco3	$$⊢\left(F:\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(S\right)\wedge x\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to \left(G\circ F\right)\left(x\right)=G\left(F\left(x\right)\right)$$
70	14 69	sylan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ x e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ x e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) ) with typecode |-
71		fvco3	$$⊢\left(F:\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(S\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to \left(G\circ F\right)\left(y\right)=G\left(F\left(y\right)\right)$$
72	14 71	sylan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ y e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ y e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) with typecode |-
73	70 72	anim12dan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) /\ ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) /\ ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) ) with typecode |-
74		oveq12	$$⊢\left(\left(G\circ F\right)\left(x\right)=G\left(F\left(x\right)\right)\wedge \left(G\circ F\right)\left(y\right)=G\left(F\left(y\right)\right)\right)\to \left(G\circ F\right)\left(x\right)1^{st}\left(T\right)\left(G\circ F\right)\left(y\right)=G\left(F\left(x\right)\right)1^{st}\left(T\right)G\left(F\left(y\right)\right)$$
75	73 74	syl	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
76	61 68 75	3eqtr4d	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) ) with typecode |-
77	9 10 17 24	rngohommul	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) with typecode |-
78	77	ex	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) with typecode |-
79	78	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) with typecode |-
80	79	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) with typecode |-
81	80	imp	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) with typecode |-
82	81	adantlrr	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) with typecode |-
83	82	fveq2d	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) = ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) = ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) with typecode |-
84	1 2 24 31	rngohommul	Could not format ( ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
85	84	ex	Could not format ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) ) with typecode |-
86	85	3expa	Could not format ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) ) with typecode |-
87	86	3adantl1	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) ) with typecode |-
88	87	imp	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
89	88	adantlrl	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
90	53 89	syldan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
91	83 90	eqtrd	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
92	9 17 10	rngocl	$$⊢\left(R\in \mathrm{RingOps}\wedge x\in \mathrm{ran}{1}^{st}\left(R\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to x{2}^{nd}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)$$
93	92	3expb	$$⊢\left(R\in \mathrm{RingOps}\wedge \left(x\in \mathrm{ran}{1}^{st}\left(R\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\right)\to x{2}^{nd}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)$$
94	93	3ad2antl1	$$⊢\left(\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge T\in \mathrm{RingOps}\right)\wedge \left(x\in \mathrm{ran}{1}^{st}\left(R\right)\wedge y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\right)\to x{2}^{nd}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)$$
95	94	adantlr	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) ) with typecode |-
96		fvco3	$$⊢\left(F:\mathrm{ran}{1}^{st}\left(R\right)⟶\mathrm{ran}{1}^{st}\left(S\right)\wedge x{2}^{nd}\left(R\right)y\in \mathrm{ran}{1}^{st}\left(R\right)\right)\to \left(G\circ F\right)\left(x{2}^{nd}\left(R\right)y\right)=G\left(F\left(x{2}^{nd}\left(R\right)y\right)\right)$$
97	14 96	sylan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) ) with typecode |-
98	95 97	syldan	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) ) with typecode |-
99		oveq12	$$⊢\left(\left(G\circ F\right)\left(x\right)=G\left(F\left(x\right)\right)\wedge \left(G\circ F\right)\left(y\right)=G\left(F\left(y\right)\right)\right)\to \left(G\circ F\right)\left(x\right)2^{nd}\left(T\right)\left(G\circ F\right)\left(y\right)=G\left(F\left(x\right)\right)2^{nd}\left(T\right)G\left(F\left(y\right)\right)$$
100	73 99	syl	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) with typecode |-
101	91 98 100	3eqtr4d	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) with typecode |-
102	76 101	jca	Could not format ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) : No typesetting found for |- ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) with typecode |-
103	102	ralrimivva	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) with typecode |-
104	9 17 10 18 3 31 4 32	isrngohom	Could not format ( ( R e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) ) with typecode |-
105	104	3adant2	Could not format ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) ) with typecode |-
106	105	adantr	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) ) with typecode |-
107	16 38 103 106	mpbir3and	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) with typecode |-