dvhopvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	dvhvadd.h	$⊢ H = LHyp (K)$
	dvhvadd.t	$⊢ T = LTrn (K) (W)$
	dvhvadd.e	$⊢ E = TEndo (K) (W)$
	dvhvadd.u	$⊢ U = DVecH (K) (W)$
	dvhvadd.f	$⊢ D = Scalar (U)$
	dvhvadd.s	$⊢ \underset{˙}{+} = +_{U}$
	dvhvadd.p	$⊢ \underset{˙}{⨣} = +_{D}$
Assertion	dvhopvadd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \underset{˙}{+} ⟨G, R⟩ = ⟨F \circ G, Q \underset{˙}{⨣} R⟩$

Proof

Step	Hyp	Ref	Expression
1		dvhvadd.h	$⊢ H = LHyp (K)$
2		dvhvadd.t	$⊢ T = LTrn (K) (W)$
3		dvhvadd.e	$⊢ E = TEndo (K) (W)$
4		dvhvadd.u	$⊢ U = DVecH (K) (W)$
5		dvhvadd.f	$⊢ D = Scalar (U)$
6		dvhvadd.s	$⊢ \underset{˙}{+} = +_{U}$
7		dvhvadd.p	$⊢ \underset{˙}{⨣} = +_{D}$
8		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to (K \in HL \land W \in H)$
9		opelxpi	$⊢ (F \in T \land Q \in E) \to ⟨F, Q⟩ \in (T \times E)$
10	9	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \in (T \times E)$
11		opelxpi	$⊢ (G \in T \land R \in E) \to ⟨G, R⟩ \in (T \times E)$
12	11	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨G, R⟩ \in (T \times E)$
13	1 2 3 4 5 6 7	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (⟨F, Q⟩ \in (T \times E) \land ⟨G, R⟩ \in (T \times E))) \to ⟨F, Q⟩ \underset{˙}{+} ⟨G, R⟩ = ⟨1^{st} (⟨F, Q⟩) \circ 1^{st} (⟨G, R⟩), 2^{nd} (⟨F, Q⟩) \underset{˙}{⨣} 2^{nd} (⟨G, R⟩)⟩$
14	8 10 12 13	syl12anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \underset{˙}{+} ⟨G, R⟩ = ⟨1^{st} (⟨F, Q⟩) \circ 1^{st} (⟨G, R⟩), 2^{nd} (⟨F, Q⟩) \underset{˙}{⨣} 2^{nd} (⟨G, R⟩)⟩$
15		op1stg	$⊢ (F \in T \land Q \in E) \to 1^{st} (⟨F, Q⟩) = F$
16	15	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to 1^{st} (⟨F, Q⟩) = F$
17		op1stg	$⊢ (G \in T \land R \in E) \to 1^{st} (⟨G, R⟩) = G$
18	17	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to 1^{st} (⟨G, R⟩) = G$
19	16 18	coeq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to 1^{st} (⟨F, Q⟩) \circ 1^{st} (⟨G, R⟩) = F \circ G$
20		op2ndg	$⊢ (F \in T \land Q \in E) \to 2^{nd} (⟨F, Q⟩) = Q$
21	20	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to 2^{nd} (⟨F, Q⟩) = Q$
22		op2ndg	$⊢ (G \in T \land R \in E) \to 2^{nd} (⟨G, R⟩) = R$
23	22	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to 2^{nd} (⟨G, R⟩) = R$
24	21 23	oveq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to 2^{nd} (⟨F, Q⟩) \underset{˙}{⨣} 2^{nd} (⟨G, R⟩) = Q \underset{˙}{⨣} R$
25	19 24	opeq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨1^{st} (⟨F, Q⟩) \circ 1^{st} (⟨G, R⟩), 2^{nd} (⟨F, Q⟩) \underset{˙}{⨣} 2^{nd} (⟨G, R⟩)⟩ = ⟨F \circ G, Q \underset{˙}{⨣} R⟩$
26	14 25	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land Q \in E) \land (G \in T \land R \in E)) \to ⟨F, Q⟩ \underset{˙}{+} ⟨G, R⟩ = ⟨F \circ G, Q \underset{˙}{⨣} R⟩$

Metamath Proof Explorer

Theorem dvhopvadd

Proof