Metamath Proof Explorer

Theorem his2sub2

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion his2sub2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB-ℎC=A⋅ihB−A⋅ihC

Proof

Step Hyp Ref Expression
1 his2sub ⊢B∈ℋ∧C∈ℋ∧A∈ℋ→B-ℎC⋅ihA=B⋅ihA−C⋅ihA
2 1 fveq2d ⊢B∈ℋ∧C∈ℋ∧A∈ℋ→B-ℎC⋅ihA‾=B⋅ihA−C⋅ihA‾
3 hicl ⊢B∈ℋ∧A∈ℋ→B⋅ihA∈ℂ
4 hicl ⊢C∈ℋ∧A∈ℋ→C⋅ihA∈ℂ
5 cjsub ⊢B⋅ihA∈ℂ∧C⋅ihA∈ℂ→B⋅ihA−C⋅ihA‾=B⋅ihA‾−C⋅ihA‾
6 3 4 5 syl2an ⊢B∈ℋ∧A∈ℋ∧C∈ℋ∧A∈ℋ→B⋅ihA−C⋅ihA‾=B⋅ihA‾−C⋅ihA‾
7 6 3impdir ⊢B∈ℋ∧C∈ℋ∧A∈ℋ→B⋅ihA−C⋅ihA‾=B⋅ihA‾−C⋅ihA‾
8 2 7 eqtrd ⊢B∈ℋ∧C∈ℋ∧A∈ℋ→B-ℎC⋅ihA‾=B⋅ihA‾−C⋅ihA‾
9 8 3comr ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→B-ℎC⋅ihA‾=B⋅ihA‾−C⋅ihA‾
10 hvsubcl ⊢B∈ℋ∧C∈ℋ→B-ℎC∈ℋ
11 ax-his1 ⊢A∈ℋ∧B-ℎC∈ℋ→A⋅ihB-ℎC=B-ℎC⋅ihA‾
12 10 11 sylan2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB-ℎC=B-ℎC⋅ihA‾
13 12 3impb ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB-ℎC=B-ℎC⋅ihA‾
14 ax-his1 ⊢A∈ℋ∧B∈ℋ→A⋅ihB=B⋅ihA‾
15 14 3adant3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB=B⋅ihA‾
16 ax-his1 ⊢A∈ℋ∧C∈ℋ→A⋅ihC=C⋅ihA‾
17 16 3adant2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihC=C⋅ihA‾
18 15 17 oveq12d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB−A⋅ihC=B⋅ihA‾−C⋅ihA‾
19 9 13 18 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB-ℎC=A⋅ihB−A⋅ihC