Metamath Proof Explorer


Theorem dvhvscaval

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

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

Proof

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