This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
50 32 49 eqtrd ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )