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 𝑌 ) ∧ 𝐺 = 𝐹 ) ) )