Metamath Proof Explorer

Theorem ringcinvALTV

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

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

Proof

Step Hyp Ref Expression
1 ringcsectALTV.c ⊢ 𝐶 = ( RingCatALTV ‘ 𝑈 )
2 ringcsectALTV.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 ringcsectALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 ringcsectALTV.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 ringcsectALTV.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 ringcinvALTV.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
7 1 ringccatALTV ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ 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 ringcsectALTV ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( 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 ringcsectALTV ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( 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 31 33 jca ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) )
35 29 34 jca ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
37 fcof1o ⊢ ( ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ ◡ 𝐹 = 𝐺 ) )
38 eqcom ⊢ ( ◡ 𝐹 = 𝐺 ↔ 𝐺 = ◡ 𝐹 )
39 38 anbi2i ⊢ ( ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ ◡ 𝐹 = 𝐺 ) ↔ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
40 37 39 sylib ⊢ ( ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
41 36 40 syl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
42 anass ⊢ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )
43 25 41 42 sylanbrc ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) )
44 4 5 jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
45 11 15 isrim ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ) )
47 46 anbi1d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ) )
49 43 48 mpbird ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
50 11 15 rimrhm ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
51 50 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
52 isrim0 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
53 44 52 syl ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
54 eleq1 ⊢ ( ◡ 𝐹 = 𝐺 → ( ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ↔ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
55 54 eqcoms ⊢ ( 𝐺 = ◡ 𝐹 → ( ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ↔ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
56 55 anbi2d ⊢ ( 𝐺 = ◡ 𝐹 → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
57 53 56 sylan9bbr ⊢ ( ( 𝐺 = ◡ 𝐹 ∧ 𝜑 ) → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
58 simpr ⊢ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) )
59 57 58 syl6bi ⊢ ( ( 𝐺 = ◡ 𝐹 ∧ 𝜑 ) → ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
60 59 com12 ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → ( ( 𝐺 = ◡ 𝐹 ∧ 𝜑 ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
61 60 expdimp ⊢ ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) → ( 𝜑 → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
62 61 impcom ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) )
63 coeq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
64 63 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
65 11 15 rimf1o ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
66 65 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
67 f1ococnv1 ⊢ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
68 66 67 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
69 64 68 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
70 51 62 69 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) )
71 53 biimpcd ⊢ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) → ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
72 71 adantr ⊢ ( ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) → ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
73 72 impcom ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
74 eleq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ↔ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
75 74 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ↔ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) )
76 75 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
77 73 76 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
78 coeq2 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
79 78 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
80 f1ococnv2 ⊢ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
81 66 80 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
82 79 81 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
83 77 69 82 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
84 70 77 83 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
85 49 84 impbida ⊢ ( 𝜑 → ( ( ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )
86 10 23 85 3bitrd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RingIso 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )