Metamath Proof Explorer

Theorem rngcinvALTV

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

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

Proof

Step Hyp Ref Expression
1 rngcsectALTV.c ⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
2 rngcsectALTV.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 rngcsectALTV.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 rngcsectALTV.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 rngcsectALTV.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 rngcinvALTV.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
7 1 rngccatALTV ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ 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 rngcsectALTV ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
13 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) )
14 12 13 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
15 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 1 2 3 5 4 15 9 rngcsectALTV ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
17 3ancoma ⊢ ( ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
18 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
19 17 18 bitri ⊢ ( ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
20 16 19 bitrdi ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
21 14 20 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) )
22 anandi ⊢ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ↔ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
23 21 22 bitrdi ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ↔ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) )
24 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) )
26 11 15 rnghmf ⊢ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
27 15 11 rnghmf ⊢ ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) )
28 26 27 anim12i ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) )
29 28 ad2antlr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) )
30 simpr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
31 30 adantl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
32 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
33 32 ad2antrl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
34 29 31 33 jca32 ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ∧ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( 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 ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
41 anass ⊢ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )
42 25 40 41 sylanbrc ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) )
43 11 15 isrngim ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ) )
44 4 5 43 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ) )
45 44 anbi1d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) ∧ 𝐺 = ◡ 𝐹 ) ) )
47 42 46 mpbird ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ) → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) )
48 11 15 rngimrnghm ⊢ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) → 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) )
49 48 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) )
50 isrngisom ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
51 4 5 50 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
52 eleq1 ⊢ ( ◡ 𝐹 = 𝐺 → ( ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ↔ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
53 52 eqcoms ⊢ ( 𝐺 = ◡ 𝐹 → ( ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ↔ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
54 53 anbi2d ⊢ ( 𝐺 = ◡ 𝐹 → ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
55 51 54 sylan9bbr ⊢ ( ( 𝐺 = ◡ 𝐹 ∧ 𝜑 ) → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
56 simpr ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) → 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) )
57 55 56 syl6bi ⊢ ( ( 𝐺 = ◡ 𝐹 ∧ 𝜑 ) → ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) → 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
58 57 com12 ⊢ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) → ( ( 𝐺 = ◡ 𝐹 ∧ 𝜑 ) → 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
59 58 expdimp ⊢ ( ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) → ( 𝜑 → 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
60 59 impcom ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) )
61 coeq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
62 61 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) )
63 11 15 rngimf1o ⊢ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) → 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
64 63 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
65 f1ococnv1 ⊢ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
67 62 66 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
68 49 60 67 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) )
69 51 biimpcd ⊢ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) → ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
70 69 adantr ⊢ ( ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) → ( 𝜑 → ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
71 70 impcom ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
72 eleq1 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ↔ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
73 72 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ↔ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
74 73 anbi2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ ◡ 𝐹 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
75 71 74 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
76 coeq2 ⊢ ( 𝐺 = ◡ 𝐹 → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
77 76 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ◡ 𝐹 ) )
78 f1ococnv2 ⊢ ( 𝐹 : ( Base ‘ 𝑋 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
79 64 78 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
80 77 79 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) )
81 75 67 80 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) )
82 68 75 81 jca31 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) → ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) )
83 47 82 impbida ⊢ ( 𝜑 → ( ( ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) ∧ ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ ( Base ‘ 𝑋 ) ) ) ∧ ( 𝐹 ∘ 𝐺 ) = ( I ↾ ( Base ‘ 𝑌 ) ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )
84 10 23 83 3bitrd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RngIsom 𝑌 ) ∧ 𝐺 = ◡ 𝐹 ) ) )