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

Metamath Proof Explorer

Theorem fmpocos

Description: Composition of two functions. Variation of fmpoco with more context in the substitution hypothesis for T . (Contributed by SN, 14-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 fmpocos.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑅 ∈ 𝐶 )
2 fmpocos.2 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) )
3 fmpocos.3 ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝐶 ↦ 𝑆 ) )
4 fmpocos.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 19 20 op1std ⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑤 ) = 𝑢 )
23 22 csbeq1d ⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
24 21 23 csbeq12dv ⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 = ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
25 24 mpompt ⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 )
26 18 25 eqtr4i ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 )
27 26 fmpt ⊢ ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑅 ) : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
28 8 27 sylibr ⊢ ( 𝜑 → ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ∈ 𝐶 )
29 2 26 eqtrdi ⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 ) )
30 28 29 3 fmptcos ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) )
31 24 csbeq1d ⊢ ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 = ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
32 31 mpompt ⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
33 nfcv ⊢ Ⅎ 𝑢 ⦋ 𝑅 / 𝑧 ⦌ 𝑆
34 nfcv ⊢ Ⅎ 𝑣 ⦋ 𝑅 / 𝑧 ⦌ 𝑆
35 nfcv ⊢ Ⅎ 𝑥 𝑆
36 13 35 nfcsbw ⊢ Ⅎ 𝑥 ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆
37 nfcv ⊢ Ⅎ 𝑦 𝑆
38 14 37 nfcsbw ⊢ Ⅎ 𝑦 ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆
39 17 csbeq1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
40 33 34 36 38 39 cbvmpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐵 ↦ ⦋ ⦋ 𝑣 / 𝑦 ⦌ ⦋ 𝑢 / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 )
41 32 40 eqtr4i ⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 )
42 4 3impb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑅 / 𝑧 ⦌ 𝑆 = 𝑇 )
43 42 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⦋ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
44 41 43 eqtrid ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ 𝑅 / 𝑧 ⦌ 𝑆 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )
45 30 44 eqtrd ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝑇 ) )