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 46012

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 7081	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ (𝑉 × 𝑊))
4		1st2nd2 8028	. . . 4 ⊢ ((𝐹‘𝑌) ∈ (𝑉 × 𝑊) → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
5	3, 4	syl 18	. . 3 ⊢ (𝜑 → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
6	5	fveq2d 6886	. 2 ⊢ (𝜑 → (𝑂‘(𝐹‘𝑌)) = (𝑂‘⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩))
7		fvco3 6982	. . 3 ⊢ ((𝐹:𝑋⟶(𝑉 × 𝑊) ∧ 𝑌 ∈ 𝑋) → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
8	1, 2, 7	syl2anc 596	. 2 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
9		df-ov 7419	. . 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 2807	1 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 ⟨cop 4593 × cxp 5657 ∘ ccom 5663 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 1^st c1st 7987 2^nd c2nd 7988

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pr 5402 ax-un 7739

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rab 3415 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-ov 7419 df-1st 7989 df-2nd 7990

This theorem is used by: cnmetcoval 46020 volicoff 46810 voliooicof 46811 hoissre 47359 hoiprodcl 47362 hoicvr 47363 hoicvrrex 47371 ovn0lem 47380 ovnhoilem1 47416 ovnhoilem2 47417 hoicoto2 47420 ovnlecvr2 47425 ovncvr2 47426 ovolval2lem 47458 ovolval5lem3 47469

W3C validator