Metamath Proof Explorer


Theorem invcoisoid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2020)

Ref Expression
Hypotheses invisoinv.b 𝐵 = ( Base ‘ 𝐶 )
invisoinv.i 𝐼 = ( Iso ‘ 𝐶 )
invisoinv.n 𝑁 = ( Inv ‘ 𝐶 )
invisoinv.c ( 𝜑𝐶 ∈ Cat )
invisoinv.x ( 𝜑𝑋𝐵 )
invisoinv.y ( 𝜑𝑌𝐵 )
invisoinv.f ( 𝜑𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
invcoisoid.1 1 = ( Id ‘ 𝐶 )
invcoisoid.o = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
Assertion invcoisoid ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) 𝐹 ) = ( 1𝑋 ) )

Proof

Step Hyp Ref Expression
1 invisoinv.b 𝐵 = ( Base ‘ 𝐶 )
2 invisoinv.i 𝐼 = ( Iso ‘ 𝐶 )
3 invisoinv.n 𝑁 = ( Inv ‘ 𝐶 )
4 invisoinv.c ( 𝜑𝐶 ∈ Cat )
5 invisoinv.x ( 𝜑𝑋𝐵 )
6 invisoinv.y ( 𝜑𝑌𝐵 )
7 invisoinv.f ( 𝜑𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8 invcoisoid.1 1 = ( Id ‘ 𝐶 )
9 invcoisoid.o = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
10 1 2 3 4 5 6 7 invisoinvr ( 𝜑𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
11 eqid ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
12 1 3 4 5 6 11 isinv ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
13 simpl ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
14 12 13 syl6bi ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
15 10 14 mpd ( 𝜑𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
16 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
18 1 16 2 4 5 6 isohom ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
19 18 7 sseldd ( 𝜑𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
20 1 16 2 4 6 5 isohom ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
21 1 3 4 5 6 2 invf ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
22 21 7 ffvelrnd ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
23 20 22 sseldd ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
24 1 16 17 8 11 4 5 6 19 23 issect2 ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ↔ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( 1𝑋 ) ) )
25 9 a1i ( 𝜑 = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
26 25 eqcomd ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) = )
27 26 oveqd ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) 𝐹 ) )
28 27 eqeq1d ( 𝜑 → ( ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( 1𝑋 ) ↔ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) 𝐹 ) = ( 1𝑋 ) ) )
29 24 28 bitrd ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ↔ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) 𝐹 ) = ( 1𝑋 ) ) )
30 15 29 mpbid ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) 𝐹 ) = ( 1𝑋 ) )