ax-hvmulid - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > ax-hvmulid		Structured version Visualization version GIF version

Axiom ax-hvmulid 30247

Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)

**Assertion**
Ref	Expression
ax-hvmulid	⊢ (𝐴 ∈ ℋ → (1 ·_ℎ 𝐴) = 𝐴)

**Detailed syntax breakdown of Axiom ax-hvmulid**
Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		chba 30160	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c1 11108	. . . 4 class 1
5		csm 30162	. . . 4 class ·_ℎ
6	4, 1, 5	co 7406	. . 3 class (1 ·_ℎ 𝐴)
7	6, 1	wceq 1542	. 2 wff (1 ·_ℎ 𝐴) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (1 ·_ℎ 𝐴) = 𝐴)

Colors of variables: wff setvar class

This axiom is referenced by: hvmul0or 30266 hvsubid 30267 hvaddsubval 30274 hv2times 30302 hvnegdii 30303 hilvc 30403 hhssnv 30505 h1de2bi 30795 h1datomi 30822 mayete3i 30969 homullid 31041 lnop0 31207 lnopaddi 31212 lnophmlem2 31258 lnfn0i 31283 lnfnaddi 31284 strlem1 31491