Metamath Proof Explorer

Theorem his5

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

Ref Expression
Assertion his5 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→B⋅ihA⋅ℎC=A‾⁢B⋅ihC

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢A∈ℂ∧C∈ℋ→A⋅ℎC∈ℋ
2 ax-his1 ⊢B∈ℋ∧A⋅ℎC∈ℋ→B⋅ihA⋅ℎC=A⋅ℎC⋅ihB‾
3 1 2 sylan2 ⊢B∈ℋ∧A∈ℂ∧C∈ℋ→B⋅ihA⋅ℎC=A⋅ℎC⋅ihB‾
4 3 3impb ⊢B∈ℋ∧A∈ℂ∧C∈ℋ→B⋅ihA⋅ℎC=A⋅ℎC⋅ihB‾
5 4 3com12 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→B⋅ihA⋅ℎC=A⋅ℎC⋅ihB‾
6 ax-his3 ⊢A∈ℂ∧C∈ℋ∧B∈ℋ→A⋅ℎC⋅ihB=A⁢C⋅ihB
7 6 3com23 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A⋅ℎC⋅ihB=A⁢C⋅ihB
8 7 fveq2d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A⋅ℎC⋅ihB‾=A⁢C⋅ihB‾
9 hicl ⊢C∈ℋ∧B∈ℋ→C⋅ihB∈ℂ
10 cjmul ⊢A∈ℂ∧C⋅ihB∈ℂ→A⁢C⋅ihB‾=A‾⁢C⋅ihB‾
11 9 10 sylan2 ⊢A∈ℂ∧C∈ℋ∧B∈ℋ→A⁢C⋅ihB‾=A‾⁢C⋅ihB‾
12 11 3impb ⊢A∈ℂ∧C∈ℋ∧B∈ℋ→A⁢C⋅ihB‾=A‾⁢C⋅ihB‾
13 12 3com23 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A⁢C⋅ihB‾=A‾⁢C⋅ihB‾
14 ax-his1 ⊢B∈ℋ∧C∈ℋ→B⋅ihC=C⋅ihB‾
15 14 3adant1 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→B⋅ihC=C⋅ihB‾
16 15 oveq2d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A‾⁢B⋅ihC=A‾⁢C⋅ihB‾
17 13 16 eqtr4d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A⁢C⋅ihB‾=A‾⁢B⋅ihC
18 5 8 17 3eqtrd ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→B⋅ihA⋅ℎC=A‾⁢B⋅ihC