HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version

Axiom ax-hvdistr2 8879
Description: Scalar multiplication distributive law
Assertion
Ref Expression
ax-hvdistr2 |- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A + B) .h C) = ((A .h C) +h (B .h C)))

Detailed syntax breakdown of Axiom ax-hvdistr2
StepHypRef Expression
1 cA . . . 4 class A
2 cc 5232 . . . 4 class CC
31, 2wcel 958 . . 3 wff A e. CC
4 cB . . . 4 class B
54, 2wcel 958 . . 3 wff B e. CC
6 cC . . . 4 class C
7 chil 8788 . . . 4 class H~
86, 7wcel 958 . . 3 wff C e. H~
93, 5, 8w3a 775 . 2 wff (A e. CC /\ B e. CC /\ C e. H~)
10 caddc 5237 . . . . 5 class +
111, 4, 10co 3963 . . . 4 class (A + B)
12 csm 8790 . . . 4 class .h
1311, 6, 12co 3963 . . 3 class ((A + B) .h C)
141, 6, 12co 3963 . . . 4 class (A .h C)
154, 6, 12co 3963 . . . 4 class (B .h C)
16 cva 8789 . . . 4 class +h
1714, 15, 16co 3963 . . 3 class ((A .h C) +h (B .h C))
1813, 17wceq 956 . 2 wff ((A + B) .h C) = ((A .h C) +h (B .h C))
199, 18wi 3 1 wff ((A e. CC /\ B e. CC /\ C e. H~) -> ((A + B) .h C) = ((A .h C) +h (B .h C)))
Colors of variables: wff set class
This axiom is referenced by:  hvsubidt 8895  hvsubdistr2t 8917  hv2timest 8928  hilvc 9029  hhssnv 9134  hoadddirt 9730  superpos 10281
Copyright terms: Public domain