This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-hvdistr2

Description: Scalar multiplication distributive law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-hvdistr2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 + 𝐵 ) ·ℎ 𝐶 ) = ( ( 𝐴 ·ℎ 𝐶 ) +ℎ ( 𝐵 ·ℎ 𝐶 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ⊢ 𝐴
1 cc ⊢ ℂ
2 0 1 wcel ⊢ 𝐴 ∈ ℂ
3 cB ⊢ 𝐵
4 3 1 wcel ⊢ 𝐵 ∈ ℂ
5 cC ⊢ 𝐶
6 chba ⊢ ℋ
7 5 6 wcel ⊢ 𝐶 ∈ ℋ
8 2 4 7 w3a ⊢ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ )
9 caddc ⊢ +
10 0 3 9 co ⊢ ( 𝐴 + 𝐵 )
11 csm ⊢ ·ℎ
12 10 5 11 co ⊢ ( ( 𝐴 + 𝐵 ) ·ℎ 𝐶 )
13 0 5 11 co ⊢ ( 𝐴 ·ℎ 𝐶 )
14 cva ⊢ +ℎ
15 3 5 11 co ⊢ ( 𝐵 ·ℎ 𝐶 )
16 13 15 14 co ⊢ ( ( 𝐴 ·ℎ 𝐶 ) +ℎ ( 𝐵 ·ℎ 𝐶 ) )
17 12 16 wceq ⊢ ( ( 𝐴 + 𝐵 ) ·ℎ 𝐶 ) = ( ( 𝐴 ·ℎ 𝐶 ) +ℎ ( 𝐵 ·ℎ 𝐶 ) )
18 8 17 wi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 + 𝐵 ) ·ℎ 𝐶 ) = ( ( 𝐴 ·ℎ 𝐶 ) +ℎ ( 𝐵 ·ℎ 𝐶 ) ) )