rngoisocnv

Description: The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

		Ref	Expression
	Assertion	rngoisocnv	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	⊢ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) )
2		f1of	⊢ ( ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) → ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) ⟶ ran ( 1^st ‘ 𝑅 ) )
3	1 2	syl	⊢ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) ⟶ ran ( 1^st ‘ 𝑅 ) )
4	3	ad2antll	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) ⟶ ran ( 1^st ‘ 𝑅 ) )
5		eqid	⊢ ( 2^nd ‘ 𝑅 ) = ( 2^nd ‘ 𝑅 )
6		eqid	⊢ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) )
7		eqid	⊢ ( 2^nd ‘ 𝑆 ) = ( 2^nd ‘ 𝑆 )
8		eqid	⊢ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) )
9	5 6 7 8	rngohom1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) )
10	9	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) )
11	10	adantrr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) )
12		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
13	12 5 6	rngo1cl	⊢ ( 𝑅 ∈ RingOps → ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
14		f1ocnvfv	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ∈ ran ( 1^st ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) )
15	13 14	sylan2	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ 𝑅 ∈ RingOps ) → ( ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) )
16	15	ancoms	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) )
17	16	ad2ant2rl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) )
18	11 17	mpd	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) )
19		f1ocnvfv2	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
20		f1ocnvfv2	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
21	19 20	anim12dan	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 ) )
22		oveq12	⊢ ( ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
23	21 22	syl	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
24	23	adantll	⊢ ( ( ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
25	24	adantll	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
26		f1ocnvdm	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) )
27		f1ocnvdm	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) )
28	26 27	anim12dan	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) )
29		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
30		eqid	⊢ ( 1^st ‘ 𝑆 ) = ( 1^st ‘ 𝑆 )
31	29 12 30	rngohomadd	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
32	28 31	sylan2	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
33	32	exp32	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → ( ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
34	33	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → ( ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
35	34	impr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) )
36	35	imp	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
37		eqid	⊢ ran ( 1^st ‘ 𝑆 ) = ran ( 1^st ‘ 𝑆 )
38	30 37	rngogcl	⊢ ( ( 𝑆 ∈ RingOps ∧ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) )
39	38	3expb	⊢ ( ( 𝑆 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) )
40		f1ocnvfv2	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
41	40	ancoms	⊢ ( ( ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
42	39 41	sylan	⊢ ( ( ( 𝑆 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
43	42	an32s	⊢ ( ( ( 𝑆 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
44	43	adantlll	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
45	44	adantlrl	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) )
46	25 36 45	3eqtr4rd	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
47		f1of1	⊢ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1→ ran ( 1^st ‘ 𝑆 ) )
48	47	ad2antlr	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1→ ran ( 1^st ‘ 𝑆 ) )
49		f1ocnvdm	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
50	49	ancoms	⊢ ( ( ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
51	39 50	sylan	⊢ ( ( ( 𝑆 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
52	51	an32s	⊢ ( ( ( 𝑆 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
53	52	adantlll	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
54	29 12	rngogcl	⊢ ( ( 𝑅 ∈ RingOps ∧ ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
55	54	3expb	⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
56	28 55	sylan2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
57	56	anassrs	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
58	57	adantllr	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
59		f1fveq	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1→ ran ( 1^st ‘ 𝑆 ) ∧ ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ↔ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
60	48 53 58 59	syl12anc	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ↔ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
61	60	adantlrl	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ↔ ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
62	46 61	mpbid	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) )
63		oveq12	⊢ ( ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 ∧ ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
64	21 63	syl	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
65	64	adantll	⊢ ( ( ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
66	65	adantll	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
67	29 12 5 7	rngohommul	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
68	28 67	sylan2	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
69	68	exp32	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → ( ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
70	69	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) → ( ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
71	70	impr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) )
72	71	imp	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑥 ) ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
73	30 7 37	rngocl	⊢ ( ( 𝑆 ∈ RingOps ∧ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) )
74	73	3expb	⊢ ( ( 𝑆 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) )
75		f1ocnvfv2	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
76	75	ancoms	⊢ ( ( ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
77	74 76	sylan	⊢ ( ( ( 𝑆 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
78	77	an32s	⊢ ( ( ( 𝑆 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
79	78	adantlll	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
80	79	adantlrl	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) )
81	66 72 80	3eqtr4rd	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
82		f1ocnvdm	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
83	82	ancoms	⊢ ( ( ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
84	74 83	sylan	⊢ ( ( ( 𝑆 ∈ RingOps ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
85	84	an32s	⊢ ( ( ( 𝑆 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
86	85	adantlll	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
87	29 5 12	rngocl	⊢ ( ( 𝑅 ∈ RingOps ∧ ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
88	87	3expb	⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( ^◡ 𝐹 ‘ 𝑥 ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ 𝑦 ) ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
89	28 88	sylan2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
90	89	anassrs	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
91	90	adantllr	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) )
92		f1fveq	⊢ ( ( 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1→ ran ( 1^st ‘ 𝑆 ) ∧ ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) ∧ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ↔ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
93	48 86 91 92	syl12anc	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ↔ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
94	93	adantlrl	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ↔ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
95	81 94	mpbid	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) )
96	62 95	jca	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) ∧ ( 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∧ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ) ) → ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
97	96	ralrimivva	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) )
98	30 7 37 8 29 5 12 6	isrngohom	⊢ ( ( 𝑆 ∈ RingOps ∧ 𝑅 ∈ RingOps ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ↔ ( ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) ⟶ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
99	98	ancoms	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ↔ ( ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) ⟶ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
100	99	adantr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ↔ ( ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) ⟶ ran ( 1^st ‘ 𝑅 ) ∧ ( ^◡ 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑆 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑆 ) ( ( ^◡ 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ^◡ 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑆 ) 𝑦 ) ) = ( ( ^◡ 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑅 ) ( ^◡ 𝐹 ‘ 𝑦 ) ) ) ) ) )
101	4 18 97 100	mpbir3and	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) )
102	1	ad2antll	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) )
103	101 102	jca	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ∧ ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) ) )
104	103	ex	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ∧ ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) ) ) )
105	29 12 30 37	isrngoiso	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : ran ( 1^st ‘ 𝑅 ) –1-1-onto→ ran ( 1^st ‘ 𝑆 ) ) ) )
106	30 37 29 12	isrngoiso	⊢ ( ( 𝑆 ∈ RingOps ∧ 𝑅 ∈ RingOps ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) ↔ ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ∧ ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) ) ) )
107	106	ancoms	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) ↔ ( ^◡ 𝐹 ∈ ( 𝑆 RngHom 𝑅 ) ∧ ^◡ 𝐹 : ran ( 1^st ‘ 𝑆 ) –1-1-onto→ ran ( 1^st ‘ 𝑅 ) ) ) )
108	104 105 107	3imtr4d	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) ) )
109	108	3impia	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → ^◡ 𝐹 ∈ ( 𝑆 RngIso 𝑅 ) )

Metamath Proof Explorer

Theorem rngoisocnv

Proof