Theorem fmpoco

Description: Composition of two functions. Variation of fmptco when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	fmpoco.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ 𝐶 )
	fmpoco.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) )
	fmpoco.3	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝐶 ↦ 𝑆 ) )
	fmpoco.4	⊢ ( 𝑧 = 𝑅 → 𝑆 = 𝑇 )
Assertion	fmpoco	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		fmpoco.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ 𝐶 )
2		fmpoco.2	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) )
3		fmpoco.3	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝐶 ↦ 𝑆 ) )
4		fmpoco.4	⊢ ( 𝑧 = 𝑅 → 𝑆 = 𝑇 )
5	1	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 )
7	6	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
8	5 7	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
9		nfcv	⊢ Ⅎ 𝑢 𝑅
10		nfcv	⊢ Ⅎ 𝑣 𝑅
11		nfcv	⊢ Ⅎ 𝑥 𝑣
12		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝑅
13	11 12	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅
14		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅
15		csbeq1a	⊢ ( 𝑥 = 𝑢 → 𝑅 = ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
16		csbeq1a	⊢ ( 𝑦 = 𝑣 → ⦋ 𝑢 / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
17	15 16	sylan9eq	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
18	9 10 13 14 17	cbvmpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
19		vex	⊢ 𝑢 ∈ V
20		vex	⊢ 𝑣 ∈ V
21	19 20	op2ndd	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd ‘ 𝑤 ) = 𝑣 )
22	21	csbeq1d	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 )
23	19 20	op1std	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑤 ) = 𝑢 )
24	23	csbeq1d	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
25	24	csbeq2dv	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ 𝑣 / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
26	22 25	eqtrd	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
27	26	mpompt	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
28	18 27	eqtr4i	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 )
29	28	fmpt	⊢ ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
30	8 29	sylibr	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ∈ 𝐶 )
31	2 28	eqtrdi	⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ) )
32	30 31 3	fmptcos	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) )
33	26	csbeq1d	⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 = ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
34	33	mpompt	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
35		nfcv	⊢ Ⅎ 𝑢 ⦋ 𝑅 / 𝑧 ⦌ 𝑆
36		nfcv	⊢ Ⅎ 𝑣 ⦋ 𝑅 / 𝑧 ⦌ 𝑆
37		nfcv	⊢ Ⅎ 𝑥 𝑆
38	13 37	nfcsbw	⊢ Ⅎ 𝑥 ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆
39		nfcv	⊢ Ⅎ 𝑦 𝑆
40	14 39	nfcsbw	⊢ Ⅎ 𝑦 ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆
41	17	csbeq1d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
42	35 36 38 40 41	cbvmpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
43	34 42	eqtr4i	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 )
44	1	3impb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑅 ∈ 𝐶 )
45		nfcvd	⊢ ( 𝑅 ∈ 𝐶 → Ⅎ 𝑧 𝑇 )
46	45 4	csbiegf	⊢ ( 𝑅 ∈ 𝐶 → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = 𝑇 )
47	44 46	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = 𝑇 )
48	47	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
49	43 48	syl5eq	⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
50	32 49	eqtrd	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )