Metamath Proof Explorer

Theorem dvhvaddval

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

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

Proof

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