HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvdistr2 Unicode version

Axiom ax-hvdistr2 22504
Description: Scalar multiplication distributive law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvdistr2

Detailed syntax breakdown of Axiom ax-hvdistr2
StepHypRef Expression
1 cA . . . 4
2 cc 8980 . . . 4
31, 2wcel 1725 . . 3
4 cB . . . 4
54, 2wcel 1725 . . 3
6 cC . . . 4
7 chil 22414 . . . 4
86, 7wcel 1725 . . 3
93, 5, 8w3a 936 . 2
10 caddc 8985 . . . . 5
111, 4, 10co 6073 . . . 4
12 csm 22416 . . . 4
1311, 6, 12co 6073 . . 3
141, 6, 12co 6073 . . . 4
154, 6, 12co 6073 . . . 4
16 cva 22415 . . . 4
1714, 15, 16co 6073 . . 3
1813, 17wceq 1652 . 2
199, 18wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hvsubid  22520  hvsubdistr2  22544  hv2times  22555  hilvc  22656  hhssnv  22756  hoadddir  23299  superpos  23849
  Copyright terms: Public domain W3C validator