Axiom ax-hvdistr1 8817

Description: Scalar multiplication distributive law

Assertion

Ref	Expression
ax-hvdistr1	⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → (A ·h (B +h C)) = ((A ·h B) +h (A ·h C)))

Detailed syntax breakdown of Axiom ax-hvdistr1

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 5212	. . . 4 class ℂ
3	1, 2	wcel 956	. . 3 wff A ∈ ℂ
4		cB	. . . 4 class B
5		chil 8727	. . . 4 class ℋ
6	4, 5	wcel 956	. . 3 wff B ∈ ℋ
7		cC	. . . 4 class C
8	7, 5	wcel 956	. . 3 wff C ∈ ℋ
9	3, 6, 8	w3a 774	. 2 wff (A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ )
10		cva 8728	. . . . 5 class +h
11	4, 7, 10	co 3954	. . . 4 class (B +h C)
12		csm 8729	. . . 4 class ·h
13	1, 11, 12	co 3954	. . 3 class (A ·h (B +h C))
14	1, 4, 12	co 3954	. . . 4 class (A ·h B)
15	1, 7, 12	co 3954	. . . 4 class (A ·h C)
16	14, 15, 10	co 3954	. . 3 class ((A ·h B) +h (A ·h C))
17	13, 16	wceq 954	. 2 wff (A ·h (B +h C)) = ((A ·h B) +h (A ·h C))
18	9, 17	wi 3	1 wff ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → (A ·h (B +h C)) = ((A ·h B) +h (A ·h C)))

This axiom is referenced by:  hvsub4t 8845  hvsubdistr1t 8855  hvdistr1 8857  hv2timest 8867  hilvc 8968  hhssnv 9073  shscl 9219  spanunsn 9442  hoadddit 9669  lnopm 9863  lnophs 9864

Copyright terms: Public domain