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 45648

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 7027	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ (𝑉 × 𝑊))
4		1st2nd2 7971	. . . 4 ⊢ ((𝐹‘𝑌) ∈ (𝑉 × 𝑊) → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
6	5	fveq2d 6832	. 2 ⊢ (𝜑 → (𝑂‘(𝐹‘𝑌)) = (𝑂‘⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩))
7		fvco3 6928	. . 3 ⊢ ((𝐹:𝑋⟶(𝑉 × 𝑊) ∧ 𝑌 ∈ 𝑋) → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
8	1, 2, 7	syl2anc 590	. 2 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
9		df-ov 7360	. . 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 2784	1 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1547 ∈ wcel 2119 ⟨cop 4562 × cxp 5617 ∘ ccom 5623 ⟶wf 6482 ‘cfv 6486 (class class class)co 7357 1^st c1st 7930 2^nd c2nd 7931

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5219 ax-nul 5229 ax-pr 5363 ax-un 7679

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4263 df-if 4456 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-br 5074 df-opab 5136 df-mpt 5155 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 6442 df-fun 6488 df-fn 6489 df-f 6490 df-fv 6494 df-ov 7360 df-1st 7932 df-2nd 7933

This theorem is referenced by: cnmetcoval 45656 volicoff 46446 voliooicof 46447 hoissre 46995 hoiprodcl 46998 hoicvr 46999 hoicvrrex 47007 ovn0lem 47016 ovnhoilem1 47052 ovnhoilem2 47053 hoicoto2 47056 ovnlecvr2 47061 ovncvr2 47062 ovolval2lem 47094 ovolval5lem3 47105

W3C validator