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 46208

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1569 ∈ wcel 2144 ⟨cop 4589 × cxp 5648 ∘ ccom 5654 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 1^st c1st 7999 2^nd c2nd 8000

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-fv 6546 df-ov 7423 df-1st 8001 df-2nd 8002

This theorem is used by: cnmetcoval 46216 volicoff 47005 voliooicof 47006 hoissre 47554 hoiprodcl 47557 hoicvr 47558 hoicvrrex 47566 ovn0lem 47575 ovnhoilem1 47611 ovnhoilem2 47612 hoicoto2 47615 ovnlecvr2 47620 ovncvr2 47621 ovolval2lem 47653 ovolval5lem3 47664

W3C validator