Step | Hyp | Ref
| Expression |
1 | | cdveca 39873 |
. 2
class
DVecA |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1541 |
. . . . 5
class π |
6 | | clh 38855 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6544 |
. . . 4
class
(LHypβπ) |
8 | | cnx 17126 |
. . . . . . . 8
class
ndx |
9 | | cbs 17144 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6544 |
. . . . . . 7
class
(Baseβndx) |
11 | 4 | cv 1541 |
. . . . . . . 8
class π€ |
12 | | cltrn 38972 |
. . . . . . . . 9
class
LTrn |
13 | 5, 12 | cfv 6544 |
. . . . . . . 8
class
(LTrnβπ) |
14 | 11, 13 | cfv 6544 |
. . . . . . 7
class
((LTrnβπ)βπ€) |
15 | 10, 14 | cop 4635 |
. . . . . 6
class
β¨(Baseβndx), ((LTrnβπ)βπ€)β© |
16 | | cplusg 17197 |
. . . . . . . 8
class
+g |
17 | 8, 16 | cfv 6544 |
. . . . . . 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 5681 |
. . . . . . . 8
class (π β π) |
23 | 18, 19, 14, 14, 22 | cmpo 7411 |
. . . . . . 7
class (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π)) |
24 | 17, 23 | cop 4635 |
. . . . . 6
class
β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β© |
25 | | csca 17200 |
. . . . . . . 8
class
Scalar |
26 | 8, 25 | cfv 6544 |
. . . . . . 7
class
(Scalarβndx) |
27 | | cedring 39624 |
. . . . . . . . 9
class
EDRing |
28 | 5, 27 | cfv 6544 |
. . . . . . . 8
class
(EDRingβπ) |
29 | 11, 28 | cfv 6544 |
. . . . . . 7
class
((EDRingβπ)βπ€) |
30 | 26, 29 | cop 4635 |
. . . . . 6
class
β¨(Scalarβndx), ((EDRingβπ)βπ€)β© |
31 | 15, 24, 30 | ctp 4633 |
. . . . 5
class
{β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} |
32 | | cvsca 17201 |
. . . . . . . 8
class
Β·π |
33 | 8, 32 | cfv 6544 |
. . . . . . 7
class (
Β·π βndx) |
34 | | vs |
. . . . . . . 8
setvar π |
35 | | ctendo 39623 |
. . . . . . . . . 10
class
TEndo |
36 | 5, 35 | cfv 6544 |
. . . . . . . . 9
class
(TEndoβπ) |
37 | 11, 36 | cfv 6544 |
. . . . . . . 8
class
((TEndoβπ)βπ€) |
38 | 34 | cv 1541 |
. . . . . . . . 9
class π |
39 | 20, 38 | cfv 6544 |
. . . . . . . 8
class (π βπ) |
40 | 34, 18, 37, 14, 39 | cmpo 7411 |
. . . . . . 7
class (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ)) |
41 | 33, 40 | cop 4635 |
. . . . . 6
class β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β© |
42 | 41 | csn 4629 |
. . . . 5
class {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©} |
43 | 31, 42 | cun 3947 |
. . . 4
class
({β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©}) |
44 | 4, 7, 43 | cmpt 5232 |
. . 3
class (π€ β (LHypβπ) β¦
({β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©})) |
45 | 2, 3, 44 | cmpt 5232 |
. 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βπ)βπ€) β¦ (π βπ))β©}))) |