Metamath Proof Explorer

Theorem ringcinv

Description: An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020)

Ref Expression
Hypotheses ringcsect.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
ringcsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
ringcsect.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
ringcsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ringcsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
ringcinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
Assertion ringcinv ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 ringcsect.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
2 ringcsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 ringcsect.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 ringcsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 ringcsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 ringcinv.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
7 1 ringccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
8 3 7 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
9 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
10 2 6 8 4 5 9 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
11 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
12 1 2 3 4 5 11 9 ringcsect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
13 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) )
14 12 13 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
15 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 1 2 3 5 4 15 9 ringcsect ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
17 3ancoma ⊢ ( ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
18 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
19 17 18 bitri ⊢ ( ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
20 16 19 bitrdi ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
21 14 20 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) )
22 anandi ⊢ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ↔ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
23 21 22 bitrdi ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) )
24 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
26 11 15 rhmf ⊢ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
27 15 11 rhmf ⊢ ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) )
28 26 27 anim12i ⊢ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) )
29 28 ad2antlr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) )
30 simpr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
31 30 adantl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
32 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
33 32 ad2antrl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
34 29 31 33 jca32 ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
36 fcof1o ⊢ ( ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ ◡ 𝐹 = 𝐺 ) )
37 eqcom ⊢ ( ◡ 𝐹 = 𝐺 ↔ 𝐺 = ◡ 𝐹 )
38 37 anbi2i ⊢ ( ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ ◡ 𝐹 = 𝐺 ) ↔ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
39 36 38 sylib ⊢ ( ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
40 35 39 syl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
41 anass ⊢ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )
42 25 40 41 sylanbrc ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) )
43 11 15 isrim ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
44 43 a1i ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ) )
45 44 anbi1d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ) )
47 42 46 mpbird ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
48 rimrhm ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
49 48 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
50 isrim0 ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
51 50 simprbi ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) )
52 eleq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ↔ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
53 51 52 syl5ibrcom ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → ( 𝐺 = ◡ 𝐹 → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
54 53 imp ⊢ ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) )
55 54 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) )
56 coeq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
57 56 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
58 11 15 rimf1o ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
59 58 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
60 f1ococnv1 ⊢ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
61 59 60 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
62 57 61 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
63 49 55 62 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) )
64 50 biimpi ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
65 64 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
66 52 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ↔ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
67 66 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
68 65 67 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
69 coeq2 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
70 69 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
71 f1ococnv2 ⊢ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
72 59 71 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
73 70 72 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
74 68 62 73 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
75 63 68 74 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
76 47 75 impbida ⊢ ( 𝜑 → ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )
77 10 23 76 3bitrd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )