dvhvscaval

Description: The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013)

		Ref	Expression
	Hypothesis	dvhvscaval.s	⊢ · = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
	Assertion	dvhvscaval	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑈 · 𝐹 ) = ⟨ ( 𝑈 ‘ ( 1^st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2^nd ‘ 𝐹 ) ) ⟩ )

Step	Hyp	Ref	Expression
1		dvhvscaval.s	⊢ · = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
2		fveq1	⊢ ( 𝑡 = 𝑈 → ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) = ( 𝑈 ‘ ( 1^st ‘ 𝑔 ) ) )
3		coeq1	⊢ ( 𝑡 = 𝑈 → ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) = ( 𝑈 ∘ ( 2^nd ‘ 𝑔 ) ) )
4	2 3	opeq12d	⊢ ( 𝑡 = 𝑈 → ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ = ⟨ ( 𝑈 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑈 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ )
5		2fveq3	⊢ ( 𝑔 = 𝐹 → ( 𝑈 ‘ ( 1^st ‘ 𝑔 ) ) = ( 𝑈 ‘ ( 1^st ‘ 𝐹 ) ) )
6		fveq2	⊢ ( 𝑔 = 𝐹 → ( 2^nd ‘ 𝑔 ) = ( 2^nd ‘ 𝐹 ) )
7	6	coeq2d	⊢ ( 𝑔 = 𝐹 → ( 𝑈 ∘ ( 2^nd ‘ 𝑔 ) ) = ( 𝑈 ∘ ( 2^nd ‘ 𝐹 ) ) )
8	5 7	opeq12d	⊢ ( 𝑔 = 𝐹 → ⟨ ( 𝑈 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑈 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ = ⟨ ( 𝑈 ‘ ( 1^st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2^nd ‘ 𝐹 ) ) ⟩ )
9	1	dvhvscacbv	⊢ · = ( 𝑡 ∈ 𝐸 , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑔 ) ) ⟩ )
10		opex	⊢ ⟨ ( 𝑈 ‘ ( 1^st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2^nd ‘ 𝐹 ) ) ⟩ ∈ V
11	4 8 9 10	ovmpo	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑈 · 𝐹 ) = ⟨ ( 𝑈 ‘ ( 1^st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2^nd ‘ 𝐹 ) ) ⟩ )

Metamath Proof Explorer