This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑓 ) ) ⟩ ) ⟩ } ) ) )