rngoisocnv

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

		Ref	Expression
	Assertion	rngoisocnv	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RngIso S)) \to F^{-1} \in (S RngIso R)$

Proof

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

Metamath Proof Explorer

Theorem rngoisocnv

Proof