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	⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) )