Detailed syntax breakdown of Definition df-lnfn
Step | Hyp | Ref
| Expression |
1 | | clf 29295 |
. 2
class
LinFn |
2 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
3 | 2 | cv 1540 |
. . . . . . . . . 10
class 𝑥 |
4 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
5 | 4 | cv 1540 |
. . . . . . . . . 10
class 𝑦 |
6 | | csm 29262 |
. . . . . . . . . 10
class
·ℎ |
7 | 3, 5, 6 | co 7268 |
. . . . . . . . 9
class (𝑥
·ℎ 𝑦) |
8 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
9 | 8 | cv 1540 |
. . . . . . . . 9
class 𝑧 |
10 | | cva 29261 |
. . . . . . . . 9
class
+ℎ |
11 | 7, 9, 10 | co 7268 |
. . . . . . . 8
class ((𝑥
·ℎ 𝑦) +ℎ 𝑧) |
12 | | vt |
. . . . . . . . 9
setvar 𝑡 |
13 | 12 | cv 1540 |
. . . . . . . 8
class 𝑡 |
14 | 11, 13 | cfv 6430 |
. . . . . . 7
class (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) |
15 | 5, 13 | cfv 6430 |
. . . . . . . . 9
class (𝑡‘𝑦) |
16 | | cmul 10860 |
. . . . . . . . 9
class
· |
17 | 3, 15, 16 | co 7268 |
. . . . . . . 8
class (𝑥 · (𝑡‘𝑦)) |
18 | 9, 13 | cfv 6430 |
. . . . . . . 8
class (𝑡‘𝑧) |
19 | | caddc 10858 |
. . . . . . . 8
class
+ |
20 | 17, 18, 19 | co 7268 |
. . . . . . 7
class ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧)) |
21 | 14, 20 | wceq 1541 |
. . . . . 6
wff (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧)) |
22 | | chba 29260 |
. . . . . 6
class
ℋ |
23 | 21, 8, 22 | wral 3065 |
. . . . 5
wff
∀𝑧 ∈
ℋ (𝑡‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧)) |
24 | 23, 4, 22 | wral 3065 |
. . . 4
wff
∀𝑦 ∈
ℋ ∀𝑧 ∈
ℋ (𝑡‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧)) |
25 | | cc 10853 |
. . . 4
class
ℂ |
26 | 24, 2, 25 | wral 3065 |
. . 3
wff
∀𝑥 ∈
ℂ ∀𝑦 ∈
ℋ ∀𝑧 ∈
ℋ (𝑡‘((𝑥
·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧)) |
27 | | cmap 8589 |
. . . 4
class
↑m |
28 | 25, 22, 27 | co 7268 |
. . 3
class (ℂ
↑m ℋ) |
29 | 26, 12, 28 | crab 3069 |
. 2
class {𝑡 ∈ (ℂ
↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))} |
30 | 1, 29 | wceq 1541 |
1
wff LinFn =
{𝑡 ∈ (ℂ
↑m ℋ) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ (𝑡‘((𝑥 ·ℎ 𝑦) +ℎ 𝑧)) = ((𝑥 · (𝑡‘𝑦)) + (𝑡‘𝑧))} |