ofrco

Description: Function relation between function compositions. (Contributed by Thierry Arnoux, 15-Jan-2026)

	Ref	Expression
Hypotheses	ofrco.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	ofrco.2	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
	ofrco.3	⊢ ( 𝜑 → 𝐻 : 𝐶 ⟶ 𝐴 )
	ofrco.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofrco.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
	ofrco.6	⊢ ( 𝜑 → 𝐹 ∘_r 𝑅 𝐺 )
Assertion	ofrco	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∘_r 𝑅 ( 𝐺 ∘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		ofrco.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		ofrco.2	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
3		ofrco.3	⊢ ( 𝜑 → 𝐻 : 𝐶 ⟶ 𝐴 )
4		ofrco.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		ofrco.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		ofrco.6	⊢ ( 𝜑 → 𝐹 ∘_r 𝑅 𝐺 )
7		fveq2	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
8		fveq2	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
9	7 8	breq12d	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
10		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
11		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
12		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
13	1 2 4 4 10 11 12	ofrfval	⊢ ( 𝜑 → ( 𝐹 ∘_r 𝑅 𝐺 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) ) )
14	6 13	mpbid	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐺 ‘ 𝑦 ) )
16	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
17	9 15 16	rspcdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
18	17	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
19		fnfco	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐻 : 𝐶 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐻 ) Fn 𝐶 )
20	1 3 19	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) Fn 𝐶 )
21		fnfco	⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐻 : 𝐶 ⟶ 𝐴 ) → ( 𝐺 ∘ 𝐻 ) Fn 𝐶 )
22	2 3 21	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐻 ) Fn 𝐶 )
23		inidm	⊢ ( 𝐶 ∩ 𝐶 ) = 𝐶
24	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐻 : 𝐶 ⟶ 𝐴 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
26	24 25	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) )
27	24 25	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
28	20 22 5 5 23 26 27	ofrfval	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ∘_r 𝑅 ( 𝐺 ∘ 𝐻 ) ↔ ∀ 𝑥 ∈ 𝐶 ( 𝐹 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑅 ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) ) )
29	18 28	mpbird	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∘_r 𝑅 ( 𝐺 ∘ 𝐻 ) )

Metamath Proof Explorer

Theorem ofrco

Proof