dvhfvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014)

	Ref	Expression
Hypotheses	dvhfvadd.h	$⊢ H = LHyp (K)$
	dvhfvadd.t	$⊢ T = LTrn (K) (W)$
	dvhfvadd.e	$⊢ E = TEndo (K) (W)$
	dvhfvadd.u	$⊢ U = DVecH (K) (W)$
	dvhfvadd.f	$⊢ D = Scalar (U)$
	dvhfvadd.p	$⊢ \underset{˙}{⨣} = +_{D}$
	dvhfvadd.a	$⊢ \underset{˙}{✚} = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩)$
	dvhfvadd.s	$⊢ \underset{˙}{+} = +_{U}$
Assertion	dvhfvadd	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = \underset{˙}{✚}$

Proof

Step	Hyp	Ref	Expression
1		dvhfvadd.h	$⊢ H = LHyp (K)$
2		dvhfvadd.t	$⊢ T = LTrn (K) (W)$
3		dvhfvadd.e	$⊢ E = TEndo (K) (W)$
4		dvhfvadd.u	$⊢ U = DVecH (K) (W)$
5		dvhfvadd.f	$⊢ D = Scalar (U)$
6		dvhfvadd.p	$⊢ \underset{˙}{⨣} = +_{D}$
7		dvhfvadd.a	$⊢ \underset{˙}{✚} = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩)$
8		dvhfvadd.s	$⊢ \underset{˙}{+} = +_{U}$
9		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
10	1 2 3 9 4	dvhset	$⊢ (K \in HL \land W \in H) \to U = \{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}$
11	10	fveq2d	$⊢ (K \in HL \land W \in H) \to +_{U} = +_{(\{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})}$
12	1 9 4 5	dvhsca	$⊢ (K \in HL \land W \in H) \to D = EDRing (K) (W)$
13	12	fveq2d	$⊢ (K \in HL \land W \in H) \to +_{D} = +_{EDRing (K) (W)}$
14	6 13	syl5eq	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⨣} = +_{EDRing (K) (W)}$
15	14	oveqd	$⊢ (K \in HL \land W \in H) \to 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g) = 2^{nd} (f) +_{EDRing (K) (W)} 2^{nd} (g)$
16	15	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land f \in (T \times E) \land g \in (T \times E)) \to 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g) = 2^{nd} (f) +_{EDRing (K) (W)} 2^{nd} (g)$
17		xp2nd	$⊢ f \in (T \times E) \to 2^{nd} (f) \in E$
18		xp2nd	$⊢ g \in (T \times E) \to 2^{nd} (g) \in E$
19	17 18	anim12i	$⊢ (f \in (T \times E) \land g \in (T \times E)) \to (2^{nd} (f) \in E \land 2^{nd} (g) \in E)$
20		eqid	$⊢ +_{EDRing (K) (W)} = +_{EDRing (K) (W)}$
21	1 2 3 9 20	erngplus	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (f) \in E \land 2^{nd} (g) \in E)) \to 2^{nd} (f) +_{EDRing (K) (W)} 2^{nd} (g) = (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))$
22	19 21	sylan2	$⊢ ((K \in HL \land W \in H) \land (f \in (T \times E) \land g \in (T \times E))) \to 2^{nd} (f) +_{EDRing (K) (W)} 2^{nd} (g) = (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))$
23	22	3impb	$⊢ ((K \in HL \land W \in H) \land f \in (T \times E) \land g \in (T \times E)) \to 2^{nd} (f) +_{EDRing (K) (W)} 2^{nd} (g) = (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))$
24	16 23	eqtrd	$⊢ ((K \in HL \land W \in H) \land f \in (T \times E) \land g \in (T \times E)) \to 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g) = (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))$
25	24	opeq2d	$⊢ ((K \in HL \land W \in H) \land f \in (T \times E) \land g \in (T \times E)) \to ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩ = ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩$
26	25	mpoeq3dva	$⊢ (K \in HL \land W \in H) \to (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩) = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)$
27	2	fvexi	$⊢ T \in V$
28	3	fvexi	$⊢ E \in V$
29	27 28	xpex	$⊢ T \times E \in V$
30	29 29	mpoex	$⊢ (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩) \in V$
31		eqid	$⊢ \{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\} = \{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}$
32	31	lmodplusg	$⊢ (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩) \in V \to (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩) = +_{(\{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})}$
33	30 32	ax-mp	$⊢ (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩) = +_{(\{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})}$
34	26 33	eqtr2di	$⊢ (K \in HL \land W \in H) \to +_{(\{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})} = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩)$
35	11 34	eqtrd	$⊢ (K \in HL \land W \in H) \to +_{U} = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) \underset{˙}{⨣} 2^{nd} (g)⟩)$
36	35 8 7	3eqtr4g	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = \underset{˙}{✚}$

Metamath Proof Explorer

Theorem dvhfvadd

Proof