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	⊢ ( ( 𝑅 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑅 𝑆 ⟨ 𝐹 , 𝑈 ⟩ ) = ⟨ ( 𝑅 ‘ 𝐹 ) , ( 𝑅 ∘ 𝑈 ) ⟩ )