Axiom ax-hvmulid 10508

Description: Scalar multiplication by one.

Assertion

Ref	Expression
ax-hvmulid	|- (A e. ~H -> (1 .h A) = A)

Detailed syntax breakdown of Axiom ax-hvmulid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 10420	. . 3 class ~H
3	1, 2	wcel 1300	. 2 wff A e. ~H
4		c1 6387	. . . 4 class 1
5		csm 10422	. . . 4 class .h
6	4, 1, 5	co 4884	. . 3 class (1 .h A)
7	6, 1	wceq 1298	. 2 wff (1 .h A) = A
8	3, 7	wi 3	1 wff (A e. ~H -> (1 .h A) = A)

This axiom is referenced by:  hvmul0or 10526  hvsubid 10527  hvaddsubval 10534  hv2times 10560  hvnegdii 10561  hilvc 10662  hhssnv 10767  projlem18 10836  h1de2bi 11110  h1datomi 11137  mayete3i 11308  mayete3OLDi 11309  homulid2 11363  lnop0 11527  lnopaddi 11532  lnophmlem2 11579  lnfn0i 11608  lnfnaddi 11609  strlem1 11822

Copyright terms: Public domain