![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > ax-hvmulid | Structured version Visualization version Unicode version |
Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-hvmulid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | chil 26621 |
. . 3
![]() ![]() | |
3 | 1, 2 | wcel 1898 |
. 2
![]() ![]() ![]() ![]() |
4 | c1 9566 |
. . . 4
![]() ![]() | |
5 | csm 26623 |
. . . 4
![]() ![]() | |
6 | 4, 1, 5 | co 6315 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6, 1 | wceq 1455 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | wi 4 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0or 26727 hvsubid 26728 hvaddsubval 26735 hv2times 26763 hvnegdii 26764 hilvc 26864 hhssnv 26964 h1de2bi 27256 h1datomi 27283 mayete3i 27430 homulid2 27502 lnop0 27668 lnopaddi 27673 lnophmlem2 27719 lnfn0i 27744 lnfnaddi 27745 strlem1 27952 |
Copyright terms: Public domain | W3C validator |