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

Axiom ax-hvdistr2 22548
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 9043 . . . 4
31, 2wcel 1728 . . 3
4 cB . . . 4
54, 2wcel 1728 . . 3
6 cC . . . 4
7 chil 22458 . . . 4
86, 7wcel 1728 . . 3
93, 5, 8w3a 937 . 2
10 caddc 9048 . . . . 5
111, 4, 10co 6133 . . . 4
12 csm 22460 . . . 4
1311, 6, 12co 6133 . . 3
141, 6, 12co 6133 . . . 4
154, 6, 12co 6133 . . . 4
16 cva 22459 . . . 4
1714, 15, 16co 6133 . . 3
1813, 17wceq 1654 . 2
199, 18wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hvsubid  22564  hvsubdistr2  22588  hv2times  22599  hilvc  22700  hhssnv  22800  hoadddir  23343  superpos  23893
  Copyright terms: Public domain W3C validator