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

Metamath Proof Explorer

Definition df-dveca

Description: Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013)

Ref Expression
Assertion df-dveca DVecA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdveca ⊢ DVecA
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 9 13 cop ⊢ ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩
15 cplusg ⊢ +g
16 8 15 cfv ⊢ ( +g ‘ ndx )
17 vf ⊢ 𝑓
18 vg ⊢ 𝑔
19 17 cv ⊢ 𝑓
20 18 cv ⊢ 𝑔
21 19 20 ccom ⊢ ( 𝑓 ∘ 𝑔 )
22 17 18 13 13 21 cmpo ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) )
23 16 22 cop ⊢ ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩
24 csca ⊢ Scalar
25 8 24 cfv ⊢ ( Scalar ‘ ndx )
26 cedring ⊢ EDRing
27 5 26 cfv ⊢ ( EDRing ‘ 𝑘 )
28 12 27 cfv ⊢ ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 )
29 25 28 cop ⊢ ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩
30 14 23 29 ctp ⊢ { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ }
31 cvsca ⊢ ·𝑠
32 8 31 cfv ⊢ ( ·𝑠 ‘ ndx )
33 vs ⊢ 𝑠
34 ctendo ⊢ TEndo
35 5 34 cfv ⊢ ( TEndo ‘ 𝑘 )
36 12 35 cfv ⊢ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 )
37 33 cv ⊢ 𝑠
38 19 37 cfv ⊢ ( 𝑠 ‘ 𝑓 )
39 33 17 36 13 38 cmpo ⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) )
40 32 39 cop ⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩
41 40 csn ⊢ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ }
42 30 41 cun ⊢ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ } )
43 3 6 42 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ } ) )
44 1 2 43 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ } ) ) )
45 0 44 wceq ⊢ DVecA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ } ) ) )