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

Axiom ax-hvdistr2 30262
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 class ๐ด
2 cc 11108 . . . 4 class โ„‚
31, 2wcel 2107 . . 3 wff ๐ด โˆˆ โ„‚
4 cB . . . 4 class ๐ต
54, 2wcel 2107 . . 3 wff ๐ต โˆˆ โ„‚
6 cC . . . 4 class ๐ถ
7 chba 30172 . . . 4 class โ„‹
86, 7wcel 2107 . . 3 wff ๐ถ โˆˆ โ„‹
93, 5, 8w3a 1088 . 2 wff (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‹)
10 caddc 11113 . . . . 5 class +
111, 4, 10co 7409 . . . 4 class (๐ด + ๐ต)
12 csm 30174 . . . 4 class ยทโ„Ž
1311, 6, 12co 7409 . . 3 class ((๐ด + ๐ต) ยทโ„Ž ๐ถ)
141, 6, 12co 7409 . . . 4 class (๐ด ยทโ„Ž ๐ถ)
154, 6, 12co 7409 . . . 4 class (๐ต ยทโ„Ž ๐ถ)
16 cva 30173 . . . 4 class +โ„Ž
1714, 15, 16co 7409 . . 3 class ((๐ด ยทโ„Ž ๐ถ) +โ„Ž (๐ต ยทโ„Ž ๐ถ))
1813, 17wceq 1542 . 2 wff ((๐ด + ๐ต) ยทโ„Ž ๐ถ) = ((๐ด ยทโ„Ž ๐ถ) +โ„Ž (๐ต ยทโ„Ž ๐ถ))
199, 18wi 4 1 wff ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‹) โ†’ ((๐ด + ๐ต) ยทโ„Ž ๐ถ) = ((๐ด ยทโ„Ž ๐ถ) +โ„Ž (๐ต ยทโ„Ž ๐ถ)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvsubid  30279  hvsubdistr2  30303  hv2times  30314  hilvc  30415  hhssnv  30517  hoadddir  31057  superpos  31607
  Copyright terms: Public domain W3C validator