dvhvaddval - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvhvaddval		Structured version Visualization version GIF version

Theorem dvhvaddval 37111

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.)

**Hypothesis**
Ref	Expression
dvhvaddval.a	⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), ((2^nd ‘𝑓) ⨣ (2^nd ‘𝑔))⟩)

**Assertion**
Ref	Expression
dvhvaddval	⊢ ((𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸)) → (𝐹 + 𝐺) = ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩)

Distinct variable groups: 𝑓,𝑔,𝐸 ⨣ ,𝑓,𝑔 𝑇,𝑓,𝑔 Allowed substitution hints: + (𝑓,𝑔) 𝐹(𝑓,𝑔) 𝐺(𝑓,𝑔)

Proof of Theorem dvhvaddval Dummy variables ℎ 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6411	. . . 4 ⊢ (ℎ = 𝐹 → (1^st ‘ℎ) = (1^st ‘𝐹))
2	1	coeq1d 5487	. . 3 ⊢ (ℎ = 𝐹 → ((1^st ‘ℎ) ∘ (1^st ‘𝑖)) = ((1^st ‘𝐹) ∘ (1^st ‘𝑖)))
3		fveq2 6411	. . . 4 ⊢ (ℎ = 𝐹 → (2^nd ‘ℎ) = (2^nd ‘𝐹))
4	3	oveq1d 6893	. . 3 ⊢ (ℎ = 𝐹 → ((2^nd ‘ℎ) ⨣ (2^nd ‘𝑖)) = ((2^nd ‘𝐹) ⨣ (2^nd ‘𝑖)))
5	2, 4	opeq12d 4601	. 2 ⊢ (ℎ = 𝐹 → ⟨((1^st ‘ℎ) ∘ (1^st ‘𝑖)), ((2^nd ‘ℎ) ⨣ (2^nd ‘𝑖))⟩ = ⟨((1^st ‘𝐹) ∘ (1^st ‘𝑖)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝑖))⟩)
6		fveq2 6411	. . . 4 ⊢ (𝑖 = 𝐺 → (1^st ‘𝑖) = (1^st ‘𝐺))
7	6	coeq2d 5488	. . 3 ⊢ (𝑖 = 𝐺 → ((1^st ‘𝐹) ∘ (1^st ‘𝑖)) = ((1^st ‘𝐹) ∘ (1^st ‘𝐺)))
8		fveq2 6411	. . . 4 ⊢ (𝑖 = 𝐺 → (2^nd ‘𝑖) = (2^nd ‘𝐺))
9	8	oveq2d 6894	. . 3 ⊢ (𝑖 = 𝐺 → ((2^nd ‘𝐹) ⨣ (2^nd ‘𝑖)) = ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺)))
10	7, 9	opeq12d 4601	. 2 ⊢ (𝑖 = 𝐺 → ⟨((1^st ‘𝐹) ∘ (1^st ‘𝑖)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝑖))⟩ = ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩)
11		dvhvaddval.a	. . 3 ⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘𝑓) ∘ (1^st ‘𝑔)), ((2^nd ‘𝑓) ⨣ (2^nd ‘𝑔))⟩)
12	11	dvhvaddcbv 37110	. 2 ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ ⟨((1^st ‘ℎ) ∘ (1^st ‘𝑖)), ((2^nd ‘ℎ) ⨣ (2^nd ‘𝑖))⟩)
13		opex 5123	. 2 ⊢ ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩ ∈ V
14	5, 10, 12, 13	ovmpt2 7030	1 ⊢ ((𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸)) → (𝐹 + 𝐺) = ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ⟨cop 4374 × cxp 5310 ∘ ccom 5316 ‘cfv 6101 (class class class)co 6878 ↦ cmpt2 6880 1^st c1st 7399 2^nd c2nd 7400

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-iota 6064 df-fun 6103 df-fv 6109 df-ov 6881 df-oprab 6882 df-mpt2 6883

This theorem is referenced by: dvhvadd 37113 dvhopaddN 37135

W3C validator