Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ofval Structured version   Visualization version   GIF version

Theorem ofval 7071
 Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval.1 (𝜑𝐹 Fn 𝐴)
offval.2 (𝜑𝐺 Fn 𝐵)
offval.3 (𝜑𝐴𝑉)
offval.4 (𝜑𝐵𝑊)
offval.5 (𝐴𝐵) = 𝑆
ofval.6 ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)
ofval.7 ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)
Assertion
Ref Expression
ofval ((𝜑𝑋𝑆) → ((𝐹𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))

Proof of Theorem ofval
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 offval.1 . . . . 5 (𝜑𝐹 Fn 𝐴)
2 offval.2 . . . . 5 (𝜑𝐺 Fn 𝐵)
3 offval.3 . . . . 5 (𝜑𝐴𝑉)
4 offval.4 . . . . 5 (𝜑𝐵𝑊)
5 offval.5 . . . . 5 (𝐴𝐵) = 𝑆
6 eqidd 2761 . . . . 5 ((𝜑𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
7 eqidd 2761 . . . . 5 ((𝜑𝑥𝐵) → (𝐺𝑥) = (𝐺𝑥))
81, 2, 3, 4, 5, 6, 7offval 7069 . . . 4 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
98fveq1d 6354 . . 3 (𝜑 → ((𝐹𝑓 𝑅𝐺)‘𝑋) = ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋))
109adantr 472 . 2 ((𝜑𝑋𝑆) → ((𝐹𝑓 𝑅𝐺)‘𝑋) = ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋))
11 fveq2 6352 . . . . 5 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
12 fveq2 6352 . . . . 5 (𝑥 = 𝑋 → (𝐺𝑥) = (𝐺𝑋))
1311, 12oveq12d 6831 . . . 4 (𝑥 = 𝑋 → ((𝐹𝑥)𝑅(𝐺𝑥)) = ((𝐹𝑋)𝑅(𝐺𝑋)))
14 eqid 2760 . . . 4 (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))
15 ovex 6841 . . . 4 ((𝐹𝑋)𝑅(𝐺𝑋)) ∈ V
1613, 14, 15fvmpt 6444 . . 3 (𝑋𝑆 → ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋) = ((𝐹𝑋)𝑅(𝐺𝑋)))
1716adantl 473 . 2 ((𝜑𝑋𝑆) → ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋) = ((𝐹𝑋)𝑅(𝐺𝑋)))
18 inss1 3976 . . . . . 6 (𝐴𝐵) ⊆ 𝐴
195, 18eqsstr3i 3777 . . . . 5 𝑆𝐴
2019sseli 3740 . . . 4 (𝑋𝑆𝑋𝐴)
21 ofval.6 . . . 4 ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)
2220, 21sylan2 492 . . 3 ((𝜑𝑋𝑆) → (𝐹𝑋) = 𝐶)
23 inss2 3977 . . . . . 6 (𝐴𝐵) ⊆ 𝐵
245, 23eqsstr3i 3777 . . . . 5 𝑆𝐵
2524sseli 3740 . . . 4 (𝑋𝑆𝑋𝐵)
26 ofval.7 . . . 4 ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)
2725, 26sylan2 492 . . 3 ((𝜑𝑋𝑆) → (𝐺𝑋) = 𝐷)
2822, 27oveq12d 6831 . 2 ((𝜑𝑋𝑆) → ((𝐹𝑋)𝑅(𝐺𝑋)) = (𝐶𝑅𝐷))
2910, 17, 283eqtrd 2798 1 ((𝜑𝑋𝑆) → ((𝐹𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))