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 ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) 〉 } ) ) ) |