Metamath Proof Explorer


Theorem dvhopspN

Description: Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dvhopsp.s 𝑆 = ( 𝑠𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st𝑓 ) ) , ( 𝑠 ∘ ( 2nd𝑓 ) ) ⟩ )
2 opelxpi ( ( 𝐹𝑇𝑈𝐸 ) → ⟨ 𝐹 , 𝑈 ⟩ ∈ ( 𝑇 × 𝐸 ) )
3 1 dvhvscaval ( ( 𝑅𝐸 ∧ ⟨ 𝐹 , 𝑈 ⟩ ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑅 𝑆𝐹 , 𝑈 ⟩ ) = ⟨ ( 𝑅 ‘ ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) , ( 𝑅 ∘ ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) ⟩ )
4 2 3 sylan2 ( ( 𝑅𝐸 ∧ ( 𝐹𝑇𝑈𝐸 ) ) → ( 𝑅 𝑆𝐹 , 𝑈 ⟩ ) = ⟨ ( 𝑅 ‘ ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) , ( 𝑅 ∘ ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) ⟩ )
5 op1stg ( ( 𝐹𝑇𝑈𝐸 ) → ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) = 𝐹 )
6 5 fveq2d ( ( 𝐹𝑇𝑈𝐸 ) → ( 𝑅 ‘ ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) = ( 𝑅𝐹 ) )
7 op2ndg ( ( 𝐹𝑇𝑈𝐸 ) → ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) = 𝑈 )
8 7 coeq2d ( ( 𝐹𝑇𝑈𝐸 ) → ( 𝑅 ∘ ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) = ( 𝑅𝑈 ) )
9 6 8 opeq12d ( ( 𝐹𝑇𝑈𝐸 ) → ⟨ ( 𝑅 ‘ ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) , ( 𝑅 ∘ ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) ⟩ = ⟨ ( 𝑅𝐹 ) , ( 𝑅𝑈 ) ⟩ )
10 9 adantl ( ( 𝑅𝐸 ∧ ( 𝐹𝑇𝑈𝐸 ) ) → ⟨ ( 𝑅 ‘ ( 1st ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) , ( 𝑅 ∘ ( 2nd ‘ ⟨ 𝐹 , 𝑈 ⟩ ) ) ⟩ = ⟨ ( 𝑅𝐹 ) , ( 𝑅𝑈 ) ⟩ )
11 4 10 eqtrd ( ( 𝑅𝐸 ∧ ( 𝐹𝑇𝑈𝐸 ) ) → ( 𝑅 𝑆𝐹 , 𝑈 ⟩ ) = ⟨ ( 𝑅𝐹 ) , ( 𝑅𝑈 ) ⟩ )