# 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 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{+}_{ℎ}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+\left({A}{\cdot }_{\mathrm{ih}}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ax-his2 ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}=\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
2 1 fveq2d ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}$
3 hicl ${⊢}\left({B}\in ℋ\wedge {A}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
4 hicl ${⊢}\left({C}\in ℋ\wedge {A}\in ℋ\right)\to {C}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
5 cjadd ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{A}\in ℂ\wedge {C}{\cdot }_{\mathrm{ih}}{A}\in ℂ\right)\to \stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}+\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
6 3 4 5 syl2an ${⊢}\left(\left({B}\in ℋ\wedge {A}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {A}\in ℋ\right)\right)\to \stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}+\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
7 6 3impdir ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}+\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
8 2 7 eqtrd ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}+\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
9 8 3comr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}+\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
10 hvaddcl ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{+}_{ℎ}{C}\in ℋ$
11 ax-his1 ${⊢}\left({A}\in ℋ\wedge {B}{+}_{ℎ}{C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{+}_{ℎ}{C}\right)=\stackrel{‾}{\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}$
12 10 11 sylan2 ${⊢}\left({A}\in ℋ\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{+}_{ℎ}{C}\right)=\stackrel{‾}{\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}$
13 12 3impb ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{+}_{ℎ}{C}\right)=\stackrel{‾}{\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}$
14 ax-his1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
15 14 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
16 ax-his1 ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{C}=\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
17 16 3adant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{C}=\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
18 15 17 oveq12d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{B}\right)+\left({A}{\cdot }_{\mathrm{ih}}{C}\right)=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}+\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
19 9 13 18 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{+}_{ℎ}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+\left({A}{\cdot }_{\mathrm{ih}}{C}\right)$