Theorem caofinvl

Description: Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014)

	Ref	Expression
Hypotheses	caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	caofinv.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	caofinv.4	⊢ ( 𝜑 → 𝑁 : 𝑆 ⟶ 𝑆 )
	caofinv.5	⊢ ( 𝜑 → 𝐺 = ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) )
	caofinvl.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑁 ‘ 𝑥 ) 𝑅 𝑥 ) = 𝐵 )
Assertion	caofinvl	⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐹 ) = ( 𝐴 × { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofinv.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		caofinv.4	⊢ ( 𝜑 → 𝑁 : 𝑆 ⟶ 𝑆 )
5		caofinv.5	⊢ ( 𝜑 → 𝐺 = ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) )
6		caofinvl.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑁 ‘ 𝑥 ) 𝑅 𝑥 ) = 𝐵 )
7	4	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑁 : 𝑆 ⟶ 𝑆 )
8	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 )
9	7 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ∈ 𝑆 )
10	5 9	fmpt3d	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
11	10	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
12	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
13		fvex	⊢ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ∈ V
14		eqid	⊢ ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) )
15	13 14	fnmpti	⊢ ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) Fn 𝐴
16	5	fneq1d	⊢ ( 𝜑 → ( 𝐺 Fn 𝐴 ↔ ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) Fn 𝐴 ) )
17	15 16	mpbiri	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
18		dffn5	⊢ ( 𝐺 Fn 𝐴 ↔ 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
19	17 18	sylib	⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
20	2	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) )
21	1 11 12 19 20	offval2	⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
22	5	fveq1d	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑤 ) = ( ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) ‘ 𝑤 ) )
23		2fveq3	⊢ ( 𝑣 = 𝑤 → ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) )
24		fvex	⊢ ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) ∈ V
25	23 14 24	fvmpt	⊢ ( 𝑤 ∈ 𝐴 → ( ( 𝑣 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝐹 ‘ 𝑣 ) ) ) ‘ 𝑤 ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) )
26	22 25	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) )
27	26	oveq1d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
28		fveq2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) )
29		id	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → 𝑥 = ( 𝐹 ‘ 𝑤 ) )
30	28 29	oveq12d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑁 ‘ 𝑥 ) 𝑅 𝑥 ) = ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
31	30	eqeq1d	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝑁 ‘ 𝑥 ) 𝑅 𝑥 ) = 𝐵 ↔ ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) = 𝐵 ) )
32	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( ( 𝑁 ‘ 𝑥 ) 𝑅 𝑥 ) = 𝐵 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑁 ‘ 𝑥 ) 𝑅 𝑥 ) = 𝐵 )
34	31 33 12	rspcdva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑤 ) ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) = 𝐵 )
35	27 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) = 𝐵 )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ 𝐵 ) )
37	21 36	eqtrd	⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ 𝐵 ) )
38		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑤 ∈ 𝐴 ↦ 𝐵 )
39	37 38	eqtr4di	⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐹 ) = ( 𝐴 × { 𝐵 } ) )