Detailed syntax breakdown of Definition df-mend
Step | Hyp | Ref
| Expression |
1 | | cmend 40703 |
. 2
class
MEndo |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑚 |
6 | | clmhm 20056 |
. . . . 5
class
LMHom |
7 | 5, 5, 6 | co 7213 |
. . . 4
class (𝑚 LMHom 𝑚) |
8 | | cnx 16744 |
. . . . . . . 8
class
ndx |
9 | | cbs 16760 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6380 |
. . . . . . 7
class
(Base‘ndx) |
11 | 4 | cv 1542 |
. . . . . . 7
class 𝑏 |
12 | 10, 11 | cop 4547 |
. . . . . 6
class
〈(Base‘ndx), 𝑏〉 |
13 | | cplusg 16802 |
. . . . . . . 8
class
+g |
14 | 8, 13 | cfv 6380 |
. . . . . . 7
class
(+g‘ndx) |
15 | | vx |
. . . . . . . 8
setvar 𝑥 |
16 | | vy |
. . . . . . . 8
setvar 𝑦 |
17 | 15 | cv 1542 |
. . . . . . . . 9
class 𝑥 |
18 | 16 | cv 1542 |
. . . . . . . . 9
class 𝑦 |
19 | 5, 13 | cfv 6380 |
. . . . . . . . . 10
class
(+g‘𝑚) |
20 | 19 | cof 7467 |
. . . . . . . . 9
class
∘f (+g‘𝑚) |
21 | 17, 18, 20 | co 7213 |
. . . . . . . 8
class (𝑥 ∘f
(+g‘𝑚)𝑦) |
22 | 15, 16, 11, 11, 21 | cmpo 7215 |
. . . . . . 7
class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦)) |
23 | 14, 22 | cop 4547 |
. . . . . 6
class
〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉 |
24 | | cmulr 16803 |
. . . . . . . 8
class
.r |
25 | 8, 24 | cfv 6380 |
. . . . . . 7
class
(.r‘ndx) |
26 | 17, 18 | ccom 5555 |
. . . . . . . 8
class (𝑥 ∘ 𝑦) |
27 | 15, 16, 11, 11, 26 | cmpo 7215 |
. . . . . . 7
class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) |
28 | 25, 27 | cop 4547 |
. . . . . 6
class
〈(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉 |
29 | 12, 23, 28 | ctp 4545 |
. . . . 5
class
{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} |
30 | | csca 16805 |
. . . . . . . 8
class
Scalar |
31 | 8, 30 | cfv 6380 |
. . . . . . 7
class
(Scalar‘ndx) |
32 | 5, 30 | cfv 6380 |
. . . . . . 7
class
(Scalar‘𝑚) |
33 | 31, 32 | cop 4547 |
. . . . . 6
class
〈(Scalar‘ndx), (Scalar‘𝑚)〉 |
34 | | cvsca 16806 |
. . . . . . . 8
class
·𝑠 |
35 | 8, 34 | cfv 6380 |
. . . . . . 7
class (
·𝑠 ‘ndx) |
36 | 32, 9 | cfv 6380 |
. . . . . . . 8
class
(Base‘(Scalar‘𝑚)) |
37 | 5, 9 | cfv 6380 |
. . . . . . . . . 10
class
(Base‘𝑚) |
38 | 17 | csn 4541 |
. . . . . . . . . 10
class {𝑥} |
39 | 37, 38 | cxp 5549 |
. . . . . . . . 9
class
((Base‘𝑚)
× {𝑥}) |
40 | 5, 34 | cfv 6380 |
. . . . . . . . . 10
class (
·𝑠 ‘𝑚) |
41 | 40 | cof 7467 |
. . . . . . . . 9
class
∘f ( ·𝑠 ‘𝑚) |
42 | 39, 18, 41 | co 7213 |
. . . . . . . 8
class
(((Base‘𝑚)
× {𝑥})
∘f ( ·𝑠 ‘𝑚)𝑦) |
43 | 15, 16, 36, 11, 42 | cmpo 7215 |
. . . . . . 7
class (𝑥 ∈
(Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦)) |
44 | 35, 43 | cop 4547 |
. . . . . 6
class 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉 |
45 | 33, 44 | cpr 4543 |
. . . . 5
class
{〈(Scalar‘ndx), (Scalar‘𝑚)〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉} |
46 | 29, 45 | cun 3864 |
. . . 4
class
({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑚)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉}) |
47 | 4, 7, 46 | csb 3811 |
. . 3
class
⦋(𝑚
LMHom 𝑚) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑚)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉}) |
48 | 2, 3, 47 | cmpt 5135 |
. 2
class (𝑚 ∈ V ↦
⦋(𝑚 LMHom
𝑚) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑚)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉})) |
49 | 1, 48 | wceq 1543 |
1
wff MEndo =
(𝑚 ∈ V ↦
⦋(𝑚 LMHom
𝑚) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑚)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉})) |