Step | Hyp | Ref
| Expression |
1 | | cmend 41907 |
. 2
class
MEndo |
2 | | vm |
. . 3
setvar π |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1540 |
. . . . 5
class π |
6 | | clmhm 20629 |
. . . . 5
class
LMHom |
7 | 5, 5, 6 | co 7408 |
. . . 4
class (π LMHom π) |
8 | | cnx 17125 |
. . . . . . . 8
class
ndx |
9 | | cbs 17143 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6543 |
. . . . . . 7
class
(Baseβndx) |
11 | 4 | cv 1540 |
. . . . . . 7
class π |
12 | 10, 11 | cop 4634 |
. . . . . 6
class
β¨(Baseβndx), πβ© |
13 | | cplusg 17196 |
. . . . . . . 8
class
+g |
14 | 8, 13 | cfv 6543 |
. . . . . . 7
class
(+gβndx) |
15 | | vx |
. . . . . . . 8
setvar π₯ |
16 | | vy |
. . . . . . . 8
setvar π¦ |
17 | 15 | cv 1540 |
. . . . . . . . 9
class π₯ |
18 | 16 | cv 1540 |
. . . . . . . . 9
class π¦ |
19 | 5, 13 | cfv 6543 |
. . . . . . . . . 10
class
(+gβπ) |
20 | 19 | cof 7667 |
. . . . . . . . 9
class
βf (+gβπ) |
21 | 17, 18, 20 | co 7408 |
. . . . . . . 8
class (π₯ βf
(+gβπ)π¦) |
22 | 15, 16, 11, 11, 21 | cmpo 7410 |
. . . . . . 7
class (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦)) |
23 | 14, 22 | cop 4634 |
. . . . . 6
class
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β© |
24 | | cmulr 17197 |
. . . . . . . 8
class
.r |
25 | 8, 24 | cfv 6543 |
. . . . . . 7
class
(.rβndx) |
26 | 17, 18 | ccom 5680 |
. . . . . . . 8
class (π₯ β π¦) |
27 | 15, 16, 11, 11, 26 | cmpo 7410 |
. . . . . . 7
class (π₯ β π, π¦ β π β¦ (π₯ β π¦)) |
28 | 25, 27 | cop 4634 |
. . . . . 6
class
β¨(.rβndx), (π₯ β π, π¦ β π β¦ (π₯ β π¦))β© |
29 | 12, 23, 28 | ctp 4632 |
. . . . 5
class
{β¨(Baseβndx), πβ©, β¨(+gβndx),
(π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} |
30 | | csca 17199 |
. . . . . . . 8
class
Scalar |
31 | 8, 30 | cfv 6543 |
. . . . . . 7
class
(Scalarβndx) |
32 | 5, 30 | cfv 6543 |
. . . . . . 7
class
(Scalarβπ) |
33 | 31, 32 | cop 4634 |
. . . . . 6
class
β¨(Scalarβndx), (Scalarβπ)β© |
34 | | cvsca 17200 |
. . . . . . . 8
class
Β·π |
35 | 8, 34 | cfv 6543 |
. . . . . . 7
class (
Β·π βndx) |
36 | 32, 9 | cfv 6543 |
. . . . . . . 8
class
(Baseβ(Scalarβπ)) |
37 | 5, 9 | cfv 6543 |
. . . . . . . . . 10
class
(Baseβπ) |
38 | 17 | csn 4628 |
. . . . . . . . . 10
class {π₯} |
39 | 37, 38 | cxp 5674 |
. . . . . . . . 9
class
((Baseβπ)
Γ {π₯}) |
40 | 5, 34 | cfv 6543 |
. . . . . . . . . 10
class (
Β·π βπ) |
41 | 40 | cof 7667 |
. . . . . . . . 9
class
βf ( Β·π βπ) |
42 | 39, 18, 41 | co 7408 |
. . . . . . . 8
class
(((Baseβπ)
Γ {π₯})
βf ( Β·π βπ)π¦) |
43 | 15, 16, 36, 11, 42 | cmpo 7410 |
. . . . . . 7
class (π₯ β
(Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
44 | 35, 43 | cop 4634 |
. . . . . 6
class β¨(
Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β© |
45 | 33, 44 | cpr 4630 |
. . . . 5
class
{β¨(Scalarβndx), (Scalarβπ)β©, β¨(
Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©} |
46 | 29, 45 | cun 3946 |
. . . 4
class
({β¨(Baseβndx), πβ©, β¨(+gβndx),
(π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) |
47 | 4, 7, 46 | csb 3893 |
. . 3
class
β¦(π
LMHom π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) |
48 | 2, 3, 47 | cmpt 5231 |
. 2
class (π β V β¦
β¦(π LMHom
π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |
49 | 1, 48 | wceq 1541 |
1
wff MEndo =
(π β V β¦
β¦(π LMHom
π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |