cocnvf1o

Description: Composing with the inverse of a bijection. (Contributed by Thierry Arnoux, 15-Jan-2026)

	Ref	Expression
Hypotheses	cocnvf1o.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	cocnvf1o.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
	cocnvf1o.3	⊢ ( 𝜑 → 𝐻 : 𝐴 –1-1-onto→ 𝐴 )
Assertion	cocnvf1o	⊢ ( 𝜑 → ( 𝐹 = ( 𝐺 ∘ 𝐻 ) ↔ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cocnvf1o.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		cocnvf1o.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
3		cocnvf1o.3	⊢ ( 𝜑 → 𝐻 : 𝐴 –1-1-onto→ 𝐴 )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 𝐺 ∘ 𝐻 ) ) → 𝐹 = ( 𝐺 ∘ 𝐻 ) )
5	4	coeq1d	⊢ ( ( 𝜑 ∧ 𝐹 = ( 𝐺 ∘ 𝐻 ) ) → ( 𝐹 ∘ ^◡ 𝐻 ) = ( ( 𝐺 ∘ 𝐻 ) ∘ ^◡ 𝐻 ) )
6		coass	⊢ ( ( 𝐺 ∘ 𝐻 ) ∘ ^◡ 𝐻 ) = ( 𝐺 ∘ ( 𝐻 ∘ ^◡ 𝐻 ) )
7	5 6	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐹 = ( 𝐺 ∘ 𝐻 ) ) → ( 𝐹 ∘ ^◡ 𝐻 ) = ( 𝐺 ∘ ( 𝐻 ∘ ^◡ 𝐻 ) ) )
8		f1ococnv2	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐴 → ( 𝐻 ∘ ^◡ 𝐻 ) = ( I ↾ 𝐴 ) )
9	3 8	syl	⊢ ( 𝜑 → ( 𝐻 ∘ ^◡ 𝐻 ) = ( I ↾ 𝐴 ) )
10	9	coeq2d	⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝐻 ∘ ^◡ 𝐻 ) ) = ( 𝐺 ∘ ( I ↾ 𝐴 ) ) )
11		fcoi1	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( 𝐺 ∘ ( I ↾ 𝐴 ) ) = 𝐺 )
12	2 11	syl	⊢ ( 𝜑 → ( 𝐺 ∘ ( I ↾ 𝐴 ) ) = 𝐺 )
13	10 12	eqtrd	⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝐻 ∘ ^◡ 𝐻 ) ) = 𝐺 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 𝐺 ∘ 𝐻 ) ) → ( 𝐺 ∘ ( 𝐻 ∘ ^◡ 𝐻 ) ) = 𝐺 )
15	7 14	eqtr2d	⊢ ( ( 𝜑 ∧ 𝐹 = ( 𝐺 ∘ 𝐻 ) ) → 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) → 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) )
17	16	coeq1d	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) → ( 𝐺 ∘ 𝐻 ) = ( ( 𝐹 ∘ ^◡ 𝐻 ) ∘ 𝐻 ) )
18		coass	⊢ ( ( 𝐹 ∘ ^◡ 𝐻 ) ∘ 𝐻 ) = ( 𝐹 ∘ ( ^◡ 𝐻 ∘ 𝐻 ) )
19	17 18	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) → ( 𝐺 ∘ 𝐻 ) = ( 𝐹 ∘ ( ^◡ 𝐻 ∘ 𝐻 ) ) )
20		f1ococnv1	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐴 → ( ^◡ 𝐻 ∘ 𝐻 ) = ( I ↾ 𝐴 ) )
21	3 20	syl	⊢ ( 𝜑 → ( ^◡ 𝐻 ∘ 𝐻 ) = ( I ↾ 𝐴 ) )
22	21	coeq2d	⊢ ( 𝜑 → ( 𝐹 ∘ ( ^◡ 𝐻 ∘ 𝐻 ) ) = ( 𝐹 ∘ ( I ↾ 𝐴 ) ) )
23		fcoi1	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )
24	1 23	syl	⊢ ( 𝜑 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )
25	22 24	eqtrd	⊢ ( 𝜑 → ( 𝐹 ∘ ( ^◡ 𝐻 ∘ 𝐻 ) ) = 𝐹 )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) → ( 𝐹 ∘ ( ^◡ 𝐻 ∘ 𝐻 ) ) = 𝐹 )
27	19 26	eqtr2d	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) → 𝐹 = ( 𝐺 ∘ 𝐻 ) )
28	15 27	impbida	⊢ ( 𝜑 → ( 𝐹 = ( 𝐺 ∘ 𝐻 ) ↔ 𝐺 = ( 𝐹 ∘ ^◡ 𝐻 ) ) )

Metamath Proof Explorer

Theorem cocnvf1o

Proof