![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > ax-hvmulid | 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 22383 |
. . 3
![]() ![]() | |
3 | 1, 2 | wcel 1721 |
. 2
![]() ![]() ![]() ![]() |
4 | c1 8955 |
. . . 4
![]() ![]() | |
5 | csm 22385 |
. . . 4
![]() ![]() | |
6 | 4, 1, 5 | co 6048 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6, 1 | wceq 1649 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | wi 4 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: hvmul0or 22488 hvsubid 22489 hvaddsubval 22496 hv2times 22524 hvnegdii 22525 hilvc 22625 hhssnv 22725 h1de2bi 23017 h1datomi 23044 mayete3i 23191 mayete3iOLD 23192 homulid2 23264 lnop0 23430 lnopaddi 23435 lnophmlem2 23481 lnfn0i 23506 lnfnaddi 23507 strlem1 23714 |
Copyright terms: Public domain | W3C validator |