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 30299
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 11110 . . . 4 class โ„‚
31, 2wcel 2106 . . 3 wff ๐ด โˆˆ โ„‚
4 cB . . . 4 class ๐ต
5 chba 30210 . . . 4 class โ„‹
64, 5wcel 2106 . . 3 wff ๐ต โˆˆ โ„‹
7 cC . . . 4 class ๐ถ
87, 5wcel 2106 . . 3 wff ๐ถ โˆˆ โ„‹
93, 6, 8w3a 1087 . 2 wff (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹)
10 cva 30211 . . . . 5 class +โ„Ž
114, 7, 10co 7411 . . . 4 class (๐ต +โ„Ž ๐ถ)
12 csm 30212 . . . 4 class ยทโ„Ž
131, 11, 12co 7411 . . 3 class (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ))
141, 4, 12co 7411 . . . 4 class (๐ด ยทโ„Ž ๐ต)
151, 7, 12co 7411 . . . 4 class (๐ด ยทโ„Ž ๐ถ)
1614, 15, 10co 7411 . . 3 class ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ))
1713, 16wceq 1541 . 2 wff (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ)) = ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ))
189, 17wi 4 1 wff ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ถ โˆˆ โ„‹) โ†’ (๐ด ยทโ„Ž (๐ต +โ„Ž ๐ถ)) = ((๐ด ยทโ„Ž ๐ต) +โ„Ž (๐ด ยทโ„Ž ๐ถ)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvsub4  30328  hvsubass  30335  hvsubdistr1  30340  hvdistr1i  30342  hv2times  30352  hilvc  30453  hhssnv  30555  shscli  30608  spanunsni  30870  hoadddi  31094  lnopmi  31291  lnophsi  31292
  Copyright terms: Public domain W3C validator