Detailed syntax breakdown of Definition df-dveca
Step | Hyp | Ref
| Expression |
1 | | cdveca 38672 |
. 2
class
DVecA |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3400 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar 𝑤 |
5 | 2 | cv 1541 |
. . . . 5
class 𝑘 |
6 | | clh 37654 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6350 |
. . . 4
class
(LHyp‘𝑘) |
8 | | cnx 16596 |
. . . . . . . 8
class
ndx |
9 | | cbs 16599 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6350 |
. . . . . . 7
class
(Base‘ndx) |
11 | 4 | cv 1541 |
. . . . . . . 8
class 𝑤 |
12 | | cltrn 37771 |
. . . . . . . . 9
class
LTrn |
13 | 5, 12 | cfv 6350 |
. . . . . . . 8
class
(LTrn‘𝑘) |
14 | 11, 13 | cfv 6350 |
. . . . . . 7
class
((LTrn‘𝑘)‘𝑤) |
15 | 10, 14 | cop 4532 |
. . . . . 6
class
〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉 |
16 | | cplusg 16681 |
. . . . . . . 8
class
+g |
17 | 8, 16 | cfv 6350 |
. . . . . . 7
class
(+g‘ndx) |
18 | | vf |
. . . . . . . 8
setvar 𝑓 |
19 | | vg |
. . . . . . . 8
setvar 𝑔 |
20 | 18 | cv 1541 |
. . . . . . . . 9
class 𝑓 |
21 | 19 | cv 1541 |
. . . . . . . . 9
class 𝑔 |
22 | 20, 21 | ccom 5539 |
. . . . . . . 8
class (𝑓 ∘ 𝑔) |
23 | 18, 19, 14, 14, 22 | cmpo 7185 |
. . . . . . 7
class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔)) |
24 | 17, 23 | cop 4532 |
. . . . . 6
class
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 |
25 | | csca 16684 |
. . . . . . . 8
class
Scalar |
26 | 8, 25 | cfv 6350 |
. . . . . . 7
class
(Scalar‘ndx) |
27 | | cedring 38423 |
. . . . . . . . 9
class
EDRing |
28 | 5, 27 | cfv 6350 |
. . . . . . . 8
class
(EDRing‘𝑘) |
29 | 11, 28 | cfv 6350 |
. . . . . . 7
class
((EDRing‘𝑘)‘𝑤) |
30 | 26, 29 | cop 4532 |
. . . . . 6
class
〈(Scalar‘ndx), ((EDRing‘𝑘)‘𝑤)〉 |
31 | 15, 24, 30 | ctp 4530 |
. . . . 5
class
{〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} |
32 | | cvsca 16685 |
. . . . . . . 8
class
·𝑠 |
33 | 8, 32 | cfv 6350 |
. . . . . . 7
class (
·𝑠 ‘ndx) |
34 | | vs |
. . . . . . . 8
setvar 𝑠 |
35 | | ctendo 38422 |
. . . . . . . . . 10
class
TEndo |
36 | 5, 35 | cfv 6350 |
. . . . . . . . 9
class
(TEndo‘𝑘) |
37 | 11, 36 | cfv 6350 |
. . . . . . . 8
class
((TEndo‘𝑘)‘𝑤) |
38 | 34 | cv 1541 |
. . . . . . . . 9
class 𝑠 |
39 | 20, 38 | cfv 6350 |
. . . . . . . 8
class (𝑠‘𝑓) |
40 | 34, 18, 37, 14, 39 | cmpo 7185 |
. . . . . . 7
class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓)) |
41 | 33, 40 | cop 4532 |
. . . . . 6
class 〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉 |
42 | 41 | csn 4526 |
. . . . 5
class {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉} |
43 | 31, 42 | cun 3851 |
. . . 4
class
({〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉}) |
44 | 4, 7, 43 | cmpt 5120 |
. . 3
class (𝑤 ∈ (LHyp‘𝑘) ↦
({〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉})) |
45 | 2, 3, 44 | cmpt 5120 |
. 2
class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
({〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |
46 | 1, 45 | wceq 1542 |
1
wff DVecA =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
({〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝑘)‘𝑤)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑠‘𝑓))〉}))) |