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

Metamath Proof Explorer

Theorem isinv2

Description: The property " F is an inverse of G ". (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses isinv2.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
isinv2.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
Assertion isinv2 ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 isinv2.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
2 isinv2.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
3 id ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )
4 1 3 invrcl ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → 𝐶 ∈ Cat )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 1 3 5 invrcl2 ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
7 4 6 jca ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) )
8 simpl ⊢ ( ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
9 2 8 sectrcl ⊢ ( ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) → 𝐶 ∈ Cat )
10 2 8 5 sectrcl2 ⊢ ( ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
11 9 10 jca ⊢ ( ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) → ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) )
12 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
13 simprl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
14 simprr ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
15 5 1 12 13 14 2 isinv ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) ) )
16 7 11 15 pm5.21nii ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) )