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

Theorem ofval 7412
 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 ((𝜑𝑋𝑆) → ((𝐹f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))

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 2822 . . . . 5 ((𝜑𝑥𝐴) → (𝐹𝑥) = (𝐹𝑥))
7 eqidd 2822 . . . . 5 ((𝜑𝑥𝐵) → (𝐺𝑥) = (𝐺𝑥))
81, 2, 3, 4, 5, 6, 7offval 7410 . . . 4 (𝜑 → (𝐹f 𝑅𝐺) = (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))))
98fveq1d 6667 . . 3 (𝜑 → ((𝐹f 𝑅𝐺)‘𝑋) = ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋))
109adantr 483 . 2 ((𝜑𝑋𝑆) → ((𝐹f 𝑅𝐺)‘𝑋) = ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋))
11 fveq2 6665 . . . . 5 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
12 fveq2 6665 . . . . 5 (𝑥 = 𝑋 → (𝐺𝑥) = (𝐺𝑋))
1311, 12oveq12d 7168 . . . 4 (𝑥 = 𝑋 → ((𝐹𝑥)𝑅(𝐺𝑥)) = ((𝐹𝑋)𝑅(𝐺𝑋)))
14 eqid 2821 . . . 4 (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥))) = (𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))
15 ovex 7183 . . . 4 ((𝐹𝑋)𝑅(𝐺𝑋)) ∈ V
1613, 14, 15fvmpt 6763 . . 3 (𝑋𝑆 → ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋) = ((𝐹𝑋)𝑅(𝐺𝑋)))
1716adantl 484 . 2 ((𝜑𝑋𝑆) → ((𝑥𝑆 ↦ ((𝐹𝑥)𝑅(𝐺𝑥)))‘𝑋) = ((𝐹𝑋)𝑅(𝐺𝑋)))
18 inss1 4205 . . . . . 6 (𝐴𝐵) ⊆ 𝐴
195, 18eqsstrri 4002 . . . . 5 𝑆𝐴
2019sseli 3963 . . . 4 (𝑋𝑆𝑋𝐴)
21 ofval.6 . . . 4 ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)
2220, 21sylan2 594 . . 3 ((𝜑𝑋𝑆) → (𝐹𝑋) = 𝐶)
23 inss2 4206 . . . . . 6 (𝐴𝐵) ⊆ 𝐵
245, 23eqsstrri 4002 . . . . 5 𝑆𝐵
2524sseli 3963 . . . 4 (𝑋𝑆𝑋𝐵)
26 ofval.7 . . . 4 ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)
2725, 26sylan2 594 . . 3 ((𝜑𝑋𝑆) → (𝐺𝑋) = 𝐷)
2822, 27oveq12d 7168 . 2 ((𝜑𝑋𝑆) → ((𝐹𝑋)𝑅(𝐺𝑋)) = (𝐶𝑅𝐷))
2910, 17, 283eqtrd 2860 1 ((𝜑𝑋𝑆) → ((𝐹f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))