Definition df-dvech

Description: Define constructed full vector space H. (Contributed by NM, 17-Oct-2013)

	Ref	Expression
Assertion	df-dvech	⊢ DVecH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩ } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvh	⊢ DVecH
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		cbs	⊢ Base
8		cnx	⊢ ndx
9	8 7	cfv	⊢ ( Base ‘ ndx )
10		cltrn	⊢ LTrn
11	5 10	cfv	⊢ ( LTrn ‘ 𝑘 )
12	3	cv	⊢ 𝑤
13	12 11	cfv	⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
14		ctendo	⊢ TEndo
15	5 14	cfv	⊢ ( TEndo ‘ 𝑘 )
16	12 15	cfv	⊢ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 )
17	13 16	cxp	⊢ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) )
18	9 17	cop	⊢ ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩
19		cplusg	⊢ +g
20	8 19	cfv	⊢ ( +g ‘ ndx )
21		vf	⊢ 𝑓
22		vg	⊢ 𝑔
23		c1st	⊢ 1st
24	21	cv	⊢ 𝑓
25	24 23	cfv	⊢ ( 1st ‘ 𝑓 )
26	22	cv	⊢ 𝑔
27	26 23	cfv	⊢ ( 1st ‘ 𝑔 )
28	25 27	ccom	⊢ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) )
29		vh	⊢ ℎ
30		c2nd	⊢ 2nd
31	24 30	cfv	⊢ ( 2nd ‘ 𝑓 )
32	29	cv	⊢ ℎ
33	32 31	cfv	⊢ ( ( 2nd ‘ 𝑓 ) ‘ ℎ )
34	26 30	cfv	⊢ ( 2nd ‘ 𝑔 )
35	32 34	cfv	⊢ ( ( 2nd ‘ 𝑔 ) ‘ ℎ )
36	33 35	ccom	⊢ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) )
37	29 13 36	cmpt	⊢ ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) )
38	28 37	cop	⊢ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩
39	21 22 17 17 38	cmpo	⊢ ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ )
40	20 39	cop	⊢ ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩
41		csca	⊢ Scalar
42	8 41	cfv	⊢ ( Scalar ‘ ndx )
43		cedring	⊢ EDRing
44	5 43	cfv	⊢ ( EDRing ‘ 𝑘 )
45	12 44	cfv	⊢ ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 )
46	42 45	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩
47	18 40 46	ctp	⊢ { ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ }
48		cvsca	⊢ ·𝑠
49	8 48	cfv	⊢ ( ·𝑠 ‘ ndx )
50		vs	⊢ 𝑠
51	50	cv	⊢ 𝑠
52	25 51	cfv	⊢ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) )
53	51 31	ccom	⊢ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) )
54	52 53	cop	⊢ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩
55	50 21 16 17 54	cmpo	⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
56	49 55	cop	⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩
57	56	csn	⊢ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩ }
58	47 57	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩ } )
59	3 6 58	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩ } ) )
60	1 2 59	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩ } ) ) )
61	0 60	wceq	⊢ DVecH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) , 𝑔 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ⟩ ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) × ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) ⟩ } ) ) )