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 30300
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 11110 . . . 4 class โ„‚
31, 2wcel 2106 . . 3 wff ๐ด โˆˆ โ„‚
4 cB . . . 4 class ๐ต
54, 2wcel 2106 . . 3 wff ๐ต โˆˆ โ„‚
6 cC . . . 4 class ๐ถ
7 chba 30210 . . . 4 class โ„‹
86, 7wcel 2106 . . 3 wff ๐ถ โˆˆ โ„‹
93, 5, 8w3a 1087 . 2 wff (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‹)
10 caddc 11115 . . . . 5 class +
111, 4, 10co 7411 . . . 4 class (๐ด + ๐ต)
12 csm 30212 . . . 4 class ยทโ„Ž
1311, 6, 12co 7411 . . 3 class ((๐ด + ๐ต) ยทโ„Ž ๐ถ)
141, 6, 12co 7411 . . . 4 class (๐ด ยทโ„Ž ๐ถ)
154, 6, 12co 7411 . . . 4 class (๐ต ยทโ„Ž ๐ถ)
16 cva 30211 . . . 4 class +โ„Ž
1714, 15, 16co 7411 . . 3 class ((๐ด ยทโ„Ž ๐ถ) +โ„Ž (๐ต ยทโ„Ž ๐ถ))
1813, 17wceq 1541 . 2 wff ((๐ด + ๐ต) ยทโ„Ž ๐ถ) = ((๐ด ยทโ„Ž ๐ถ) +โ„Ž (๐ต ยทโ„Ž ๐ถ))
199, 18wi 4 1 wff ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‹) โ†’ ((๐ด + ๐ต) ยทโ„Ž ๐ถ) = ((๐ด ยทโ„Ž ๐ถ) +โ„Ž (๐ต ยทโ„Ž ๐ถ)))
Colors of variables: wff setvar class
This axiom is referenced by:  hvsubid  30317  hvsubdistr2  30341  hv2times  30352  hilvc  30453  hhssnv  30555  hoadddir  31095  superpos  31645
  Copyright terms: Public domain W3C validator