dvhopvsca

Description: Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypotheses	dvhfvsca.h	$⊢ H = LHyp (K)$
	dvhfvsca.t	$⊢ T = LTrn (K) (W)$
	dvhfvsca.e	$⊢ E = TEndo (K) (W)$
	dvhfvsca.u	$⊢ U = DVecH (K) (W)$
	dvhfvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
Assertion	dvhopvsca	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to R \underset{˙}{\cdot} ⟨F, X⟩ = ⟨R (F), R \circ X⟩$

Proof

Step	Hyp	Ref	Expression
1		dvhfvsca.h	$⊢ H = LHyp (K)$
2		dvhfvsca.t	$⊢ T = LTrn (K) (W)$
3		dvhfvsca.e	$⊢ E = TEndo (K) (W)$
4		dvhfvsca.u	$⊢ U = DVecH (K) (W)$
5		dvhfvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
6		simpl	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to (K \in V \land W \in H)$
7		simpr1	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to R \in E$
8		simpr2	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to F \in T$
9		simpr3	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to X \in E$
10		opelxpi	$⊢ (F \in T \land X \in E) \to ⟨F, X⟩ \in (T \times E)$
11	8 9 10	syl2anc	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to ⟨F, X⟩ \in (T \times E)$
12	1 2 3 4 5	dvhvsca	$⊢ ((K \in V \land W \in H) \land (R \in E \land ⟨F, X⟩ \in (T \times E))) \to R \underset{˙}{\cdot} ⟨F, X⟩ = ⟨R (1^{st} (⟨F, X⟩)), R \circ 2^{nd} (⟨F, X⟩)⟩$
13	6 7 11 12	syl12anc	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to R \underset{˙}{\cdot} ⟨F, X⟩ = ⟨R (1^{st} (⟨F, X⟩)), R \circ 2^{nd} (⟨F, X⟩)⟩$
14		op1stg	$⊢ (F \in T \land X \in E) \to 1^{st} (⟨F, X⟩) = F$
15	8 9 14	syl2anc	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to 1^{st} (⟨F, X⟩) = F$
16	15	fveq2d	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to R (1^{st} (⟨F, X⟩)) = R (F)$
17		op2ndg	$⊢ (F \in T \land X \in E) \to 2^{nd} (⟨F, X⟩) = X$
18	8 9 17	syl2anc	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to 2^{nd} (⟨F, X⟩) = X$
19	18	coeq2d	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to R \circ 2^{nd} (⟨F, X⟩) = R \circ X$
20	16 19	opeq12d	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to ⟨R (1^{st} (⟨F, X⟩)), R \circ 2^{nd} (⟨F, X⟩)⟩ = ⟨R (F), R \circ X⟩$
21	13 20	eqtrd	$⊢ ((K \in V \land W \in H) \land (R \in E \land F \in T \land X \in E)) \to R \underset{˙}{\cdot} ⟨F, X⟩ = ⟨R (F), R \circ X⟩$

Metamath Proof Explorer

Theorem dvhopvsca

Proof