Step | Hyp | Ref
| Expression |
1 | | cmend 41545 |
. 2
class
MEndo |
2 | | vm |
. . 3
setvar π |
3 | | cvv 3444 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π |
6 | | clmhm 20495 |
. . . . 5
class
LMHom |
7 | 5, 5, 6 | co 7358 |
. . . 4
class (π LMHom π) |
8 | | cnx 17070 |
. . . . . . . 8
class
ndx |
9 | | cbs 17088 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6497 |
. . . . . . 7
class
(Baseβndx) |
11 | 4 | cv 1541 |
. . . . . . 7
class π |
12 | 10, 11 | cop 4593 |
. . . . . 6
class
β¨(Baseβndx), πβ© |
13 | | cplusg 17138 |
. . . . . . . 8
class
+g |
14 | 8, 13 | cfv 6497 |
. . . . . . 7
class
(+gβndx) |
15 | | vx |
. . . . . . . 8
setvar π₯ |
16 | | vy |
. . . . . . . 8
setvar π¦ |
17 | 15 | cv 1541 |
. . . . . . . . 9
class π₯ |
18 | 16 | cv 1541 |
. . . . . . . . 9
class π¦ |
19 | 5, 13 | cfv 6497 |
. . . . . . . . . 10
class
(+gβπ) |
20 | 19 | cof 7616 |
. . . . . . . . 9
class
βf (+gβπ) |
21 | 17, 18, 20 | co 7358 |
. . . . . . . 8
class (π₯ βf
(+gβπ)π¦) |
22 | 15, 16, 11, 11, 21 | cmpo 7360 |
. . . . . . 7
class (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦)) |
23 | 14, 22 | cop 4593 |
. . . . . 6
class
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β© |
24 | | cmulr 17139 |
. . . . . . . 8
class
.r |
25 | 8, 24 | cfv 6497 |
. . . . . . 7
class
(.rβndx) |
26 | 17, 18 | ccom 5638 |
. . . . . . . 8
class (π₯ β π¦) |
27 | 15, 16, 11, 11, 26 | cmpo 7360 |
. . . . . . 7
class (π₯ β π, π¦ β π β¦ (π₯ β π¦)) |
28 | 25, 27 | cop 4593 |
. . . . . 6
class
β¨(.rβndx), (π₯ β π, π¦ β π β¦ (π₯ β π¦))β© |
29 | 12, 23, 28 | ctp 4591 |
. . . . 5
class
{β¨(Baseβndx), πβ©, β¨(+gβndx),
(π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} |
30 | | csca 17141 |
. . . . . . . 8
class
Scalar |
31 | 8, 30 | cfv 6497 |
. . . . . . 7
class
(Scalarβndx) |
32 | 5, 30 | cfv 6497 |
. . . . . . 7
class
(Scalarβπ) |
33 | 31, 32 | cop 4593 |
. . . . . 6
class
β¨(Scalarβndx), (Scalarβπ)β© |
34 | | cvsca 17142 |
. . . . . . . 8
class
Β·π |
35 | 8, 34 | cfv 6497 |
. . . . . . 7
class (
Β·π βndx) |
36 | 32, 9 | cfv 6497 |
. . . . . . . 8
class
(Baseβ(Scalarβπ)) |
37 | 5, 9 | cfv 6497 |
. . . . . . . . . 10
class
(Baseβπ) |
38 | 17 | csn 4587 |
. . . . . . . . . 10
class {π₯} |
39 | 37, 38 | cxp 5632 |
. . . . . . . . 9
class
((Baseβπ)
Γ {π₯}) |
40 | 5, 34 | cfv 6497 |
. . . . . . . . . 10
class (
Β·π βπ) |
41 | 40 | cof 7616 |
. . . . . . . . 9
class
βf ( Β·π βπ) |
42 | 39, 18, 41 | co 7358 |
. . . . . . . 8
class
(((Baseβπ)
Γ {π₯})
βf ( Β·π βπ)π¦) |
43 | 15, 16, 36, 11, 42 | cmpo 7360 |
. . . . . . 7
class (π₯ β
(Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
44 | 35, 43 | cop 4593 |
. . . . . 6
class β¨(
Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β© |
45 | 33, 44 | cpr 4589 |
. . . . 5
class
{β¨(Scalarβndx), (Scalarβπ)β©, β¨(
Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©} |
46 | 29, 45 | cun 3909 |
. . . 4
class
({β¨(Baseβndx), πβ©, β¨(+gβndx),
(π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) |
47 | 4, 7, 46 | csb 3856 |
. . 3
class
β¦(π
LMHom π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) |
48 | 2, 3, 47 | cmpt 5189 |
. 2
class (π β V β¦
β¦(π LMHom
π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |
49 | 1, 48 | wceq 1542 |
1
wff MEndo =
(π β V β¦
β¦(π LMHom
π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |