Theorem caofidlcan

Description: Transfer a cancellation/identity law to the function operation. (Contributed by SN, 16-Oct-2025)

	Ref	Expression
Hypotheses	caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	caofcom.3	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
	caofidlcan.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 𝑅 𝑦 ) = 𝑦 ↔ 𝑥 = 0 ) )
Assertion	caofidlcan	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) = 𝐺 ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofcom.3	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4		caofidlcan.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 𝑅 𝑦 ) = 𝑦 ↔ 𝑥 = 0 ) )
5	2	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
6	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
7	5 6	jca	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) )
8	4	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ) = 𝑦 ↔ 𝑥 = 0 ) )
9		oveq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝑦 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) )
10	9	eqeq1d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝑦 ) = 𝑦 ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) = 𝑦 ) )
11		eqeq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 = 0 ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) )
12	10 11	bibi12d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝑥 𝑅 𝑦 ) = 𝑦 ↔ 𝑥 = 0 ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) ) )
13		oveq2	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
14		id	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → 𝑦 = ( 𝐺 ‘ 𝑤 ) )
15	13 14	eqeq12d	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) = 𝑦 ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ) )
16	15	bibi1d	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) ) )
17	12 16	rspc2v	⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ) = 𝑦 ↔ 𝑥 = 0 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) ) )
18	8 17	mpan9	⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) )
19	7 18	syldan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) = 0 ) )
20	19	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 0 ) )
21		ovexd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ∈ V )
22	21	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ∈ V )
23		mpteqb	⊢ ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ∈ V → ( ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ) )
24	22 23	syl	⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( 𝐺 ‘ 𝑤 ) ) )
25	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
26		mpteqb	⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 → ( ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) = ( 𝑤 ∈ 𝐴 ↦ 0 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 0 ) )
27	25 26	syl	⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) = ( 𝑤 ∈ 𝐴 ↦ 0 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 0 ) )
28	20 24 27	3bitr4d	⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ↔ ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) = ( 𝑤 ∈ 𝐴 ↦ 0 ) ) )
29	2	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) )
30	3	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
31	1 5 6 29 30	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) )
32	31 30	eqeq12d	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) = 𝐺 ↔ ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ) )
33		fconstmpt	⊢ ( 𝐴 × { 0 } ) = ( 𝑤 ∈ 𝐴 ↦ 0 )
34	33	a1i	⊢ ( 𝜑 → ( 𝐴 × { 0 } ) = ( 𝑤 ∈ 𝐴 ↦ 0 ) )
35	29 34	eqeq12d	⊢ ( 𝜑 → ( 𝐹 = ( 𝐴 × { 0 } ) ↔ ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) = ( 𝑤 ∈ 𝐴 ↦ 0 ) ) )
36	28 32 35	3bitr4d	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) = 𝐺 ↔ 𝐹 = ( 𝐴 × { 0 } ) ) )