Metamath Proof Explorer

Theorem his7

Description: Distributive law for inner product. Lemma 3.1(S7) of Beran p. 95. (Contributed by NM, 31-Jul-1999) (New usage is discouraged.)

Ref Expression
Assertion his7 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A⋅ihB+ℎC=A⋅ihB+A⋅ihC

Proof

Step Hyp Ref Expression
1 ax-his2 ⊢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 cjadd ⊢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 hvaddcl ⊢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