fvovco - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fvovco		Structured version Visualization version GIF version

Theorem fvovco 45191

Description: Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

**Hypotheses**
Ref	Expression
fvovco.1	⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊))
fvovco.2	⊢ (𝜑 → 𝑌 ∈ 𝑋)

**Assertion**
Ref	Expression
fvovco	⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))))

**Proof of Theorem fvovco**
Step	Hyp	Ref	Expression
1		fvovco.1	. . . . 5 ⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊))
2		fvovco.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
3	1, 2	ffvelcdmd 7019	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ (𝑉 × 𝑊))
4		1st2nd2 7963	. . . 4 ⊢ ((𝐹‘𝑌) ∈ (𝑉 × 𝑊) → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
6	5	fveq2d 6826	. 2 ⊢ (𝜑 → (𝑂‘(𝐹‘𝑌)) = (𝑂‘⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩))
7		fvco3 6922	. . 3 ⊢ ((𝐹:𝑋⟶(𝑉 × 𝑊) ∧ 𝑌 ∈ 𝑋) → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
8	1, 2, 7	syl2anc 584	. 2 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
9		df-ov 7352	. . 3 ⊢ ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))) = (𝑂‘⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
10	9	a1i 11	. 2 ⊢ (𝜑 → ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))) = (𝑂‘⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩))
11	6, 8, 10	3eqtr4d 2774	1 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 ⟨cop 4583 × cxp 5617 ∘ ccom 5623 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 1^st c1st 7922 2^nd c2nd 7923

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3395 df-v 3438 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-br 5093 df-opab 5155 df-mpt 5174 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-fv 6490 df-ov 7352 df-1st 7924 df-2nd 7925

This theorem is referenced by: cnmetcoval 45200 volicoff 45996 voliooicof 45997 hoissre 46545 hoiprodcl 46548 hoicvr 46549 hoicvrrex 46557 ovn0lem 46566 ovnhoilem1 46602 ovnhoilem2 46603 hoicoto2 46606 ovnlecvr2 46611 ovncvr2 46612 ovolval2lem 46644 ovolval5lem3 46655

W3C validator