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

Axiom ax-hvdistr1 30261
Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvdistr1 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹) โ†’ (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ)) = ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ)))

Detailed syntax breakdown of Axiom ax-hvdistr1
StepHypRef Expression
1 cA . . . 4 class ๐ด
2 cc 11108 . . . 4 class โ„‚
31, 2wcel 2107 . . 3 wff ๐ด โˆˆ โ„‚
4 cB . . . 4 class ๐ต
5 chba 30172 . . . 4 class โ„‹
64, 5wcel 2107 . . 3 wff ๐ต โˆˆ โ„‹
7 cC . . . 4 class ๐ถ
87, 5wcel 2107 . . 3 wff ๐ถ โˆˆ โ„‹
93, 6, 8w3a 1088 . 2 wff (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹)
10 cva 30173 . . . . 5 class +โ„Ž
114, 7, 10co 7409 . . . 4 class (๐ต +โ„Ž ๐ถ)
12 csm 30174 . . . 4 class ยทโ„Ž
131, 11, 12co 7409 . . 3 class (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ))
141, 4, 12co 7409 . . . 4 class (๐ด ยทโ„Ž ๐ต)
151, 7, 12co 7409 . . . 4 class (๐ด ยทโ„Ž ๐ถ)
1614, 15, 10co 7409 . . 3 class ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ))
1713, 16wceq 1542 . 2 wff (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ)) = ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ))
189, 17wi 4 1 wff ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹) โ†’ (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ)) = ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvsub4  30290  hvsubass  30297  hvsubdistr1  30302  hvdistr1i  30304  hv2times  30314  hilvc  30415  hhssnv  30517  shscli  30570  spanunsni  30832  hoadddi  31056  lnopmi  31253  lnophsi  31254
  Copyright terms: Public domain W3C validator