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 45776

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 7068	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ (𝑉 × 𝑊))
4		1st2nd2 8011	. . . 4 ⊢ ((𝐹‘𝑌) ∈ (𝑉 × 𝑊) → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘𝑌) = ⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩)
6	5	fveq2d 6873	. 2 ⊢ (𝜑 → (𝑂‘(𝐹‘𝑌)) = (𝑂‘⟨(1^st ‘(𝐹‘𝑌)), (2^nd ‘(𝐹‘𝑌))⟩))
7		fvco3 6969	. . 3 ⊢ ((𝐹:𝑋⟶(𝑉 × 𝑊) ∧ 𝑌 ∈ 𝑋) → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
8	1, 2, 7	syl2anc 593	. 2 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = (𝑂‘(𝐹‘𝑌)))
9		df-ov 7401	. . 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 2809	1 ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1^st ‘(𝐹‘𝑌))𝑂(2^nd ‘(𝐹‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1562 ∈ wcel 2144 ⟨cop 4590 × cxp 5647 ∘ ccom 5653 ⟶wf 6519 ‘cfv 6523 (class class class)co 7398 1^st c1st 7970 2^nd c2nd 7971

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-sep 5248 ax-nul 5258 ax-pr 5392 ax-un 7720

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3079 df-rex 3089 df-rab 3417 df-v 3458 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5544 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-fv 6531 df-ov 7401 df-1st 7972 df-2nd 7973

This theorem is referenced by: cnmetcoval 45784 volicoff 46574 voliooicof 46575 hoissre 47123 hoiprodcl 47126 hoicvr 47127 hoicvrrex 47135 ovn0lem 47144 ovnhoilem1 47180 ovnhoilem2 47181 hoicoto2 47184 ovnlecvr2 47189 ovncvr2 47190 ovolval2lem 47222 ovolval5lem3 47233

W3C validator