Step | Hyp | Ref
| Expression |
1 | | clfn 37927 |
. 2
class
LFnl |
2 | | vw |
. . 3
setvar π€ |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vr |
. . . . . . . . . . . 12
setvar π |
5 | 4 | cv 1541 |
. . . . . . . . . . 11
class π |
6 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
7 | 6 | cv 1541 |
. . . . . . . . . . 11
class π₯ |
8 | 2 | cv 1541 |
. . . . . . . . . . . 12
class π€ |
9 | | cvsca 17201 |
. . . . . . . . . . . 12
class
Β·π |
10 | 8, 9 | cfv 6544 |
. . . . . . . . . . 11
class (
Β·π βπ€) |
11 | 5, 7, 10 | co 7409 |
. . . . . . . . . 10
class (π(
Β·π βπ€)π₯) |
12 | | vy |
. . . . . . . . . . 11
setvar π¦ |
13 | 12 | cv 1541 |
. . . . . . . . . 10
class π¦ |
14 | | cplusg 17197 |
. . . . . . . . . . 11
class
+g |
15 | 8, 14 | cfv 6544 |
. . . . . . . . . 10
class
(+gβπ€) |
16 | 11, 13, 15 | co 7409 |
. . . . . . . . 9
class ((π(
Β·π βπ€)π₯)(+gβπ€)π¦) |
17 | | vf |
. . . . . . . . . 10
setvar π |
18 | 17 | cv 1541 |
. . . . . . . . 9
class π |
19 | 16, 18 | cfv 6544 |
. . . . . . . 8
class (πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) |
20 | 7, 18 | cfv 6544 |
. . . . . . . . . 10
class (πβπ₯) |
21 | | csca 17200 |
. . . . . . . . . . . 12
class
Scalar |
22 | 8, 21 | cfv 6544 |
. . . . . . . . . . 11
class
(Scalarβπ€) |
23 | | cmulr 17198 |
. . . . . . . . . . 11
class
.r |
24 | 22, 23 | cfv 6544 |
. . . . . . . . . 10
class
(.rβ(Scalarβπ€)) |
25 | 5, 20, 24 | co 7409 |
. . . . . . . . 9
class (π(.rβ(Scalarβπ€))(πβπ₯)) |
26 | 13, 18 | cfv 6544 |
. . . . . . . . 9
class (πβπ¦) |
27 | 22, 14 | cfv 6544 |
. . . . . . . . 9
class
(+gβ(Scalarβπ€)) |
28 | 25, 26, 27 | co 7409 |
. . . . . . . 8
class ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦)) |
29 | 19, 28 | wceq 1542 |
. . . . . . 7
wff (πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦)) |
30 | | cbs 17144 |
. . . . . . . 8
class
Base |
31 | 8, 30 | cfv 6544 |
. . . . . . 7
class
(Baseβπ€) |
32 | 29, 12, 31 | wral 3062 |
. . . . . 6
wff
βπ¦ β
(Baseβπ€)(πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦)) |
33 | 32, 6, 31 | wral 3062 |
. . . . 5
wff
βπ₯ β
(Baseβπ€)βπ¦ β (Baseβπ€)(πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦)) |
34 | 22, 30 | cfv 6544 |
. . . . 5
class
(Baseβ(Scalarβπ€)) |
35 | 33, 4, 34 | wral 3062 |
. . . 4
wff
βπ β
(Baseβ(Scalarβπ€))βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)(πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦)) |
36 | | cmap 8820 |
. . . . 5
class
βm |
37 | 34, 31, 36 | co 7409 |
. . . 4
class
((Baseβ(Scalarβπ€)) βm (Baseβπ€)) |
38 | 35, 17, 37 | crab 3433 |
. . 3
class {π β
((Baseβ(Scalarβπ€)) βm (Baseβπ€)) β£ βπ β
(Baseβ(Scalarβπ€))βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)(πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦))} |
39 | 2, 3, 38 | cmpt 5232 |
. 2
class (π€ β V β¦ {π β
((Baseβ(Scalarβπ€)) βm (Baseβπ€)) β£ βπ β
(Baseβ(Scalarβπ€))βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)(πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦))}) |
40 | 1, 39 | wceq 1542 |
1
wff LFnl =
(π€ β V β¦ {π β
((Baseβ(Scalarβπ€)) βm (Baseβπ€)) β£ βπ β
(Baseβ(Scalarβπ€))βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)(πβ((π( Β·π
βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦))}) |