This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isocoinvid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-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 ‘ 𝐶 )
isocoinvid.o ⊢ ⚬ = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
Assertion isocoinvid ( 𝜑 → ( 𝐹 ⚬ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 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 isocoinvid.o ⊢ ⚬ = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
10 1 2 3 4 5 6 7 invisoinvl ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )
11 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
12 1 3 4 6 5 11 isinv ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 ↔ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) ) )
13 simpl ⊢ ( ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
14 12 13 biimtrdi ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
15 10 14 mpd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
16 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
18 1 16 2 4 6 5 isohom ⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
19 1 3 4 5 6 2 invf ⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
20 19 7 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
21 18 20 sseldd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
22 1 16 2 4 5 6 isohom ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
23 22 7 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
24 1 16 17 8 11 4 6 5 21 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 ‘ 𝑌 ) )