# Metamath Proof Explorer

## Axiom ax-his2

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

Ref Expression
Assertion ax-his2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 chba ${class}ℋ$
2 0 1 wcel ${wff}{A}\in ℋ$
3 cB ${class}{B}$
4 3 1 wcel ${wff}{B}\in ℋ$
5 cC ${class}{C}$
6 5 1 wcel ${wff}{C}\in ℋ$
7 2 4 6 w3a ${wff}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)$
8 cva ${class}{+}_{ℎ}$
9 0 3 8 co ${class}\left({A}{+}_{ℎ}{B}\right)$
10 csp ${class}{\cdot }_{\mathrm{ih}}$
11 9 5 10 co ${class}\left(\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)$
12 0 5 10 co ${class}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)$
13 caddc ${class}+$
14 3 5 10 co ${class}\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
15 12 14 13 co ${class}\left(\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
16 11 15 wceq ${wff}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
17 7 16 wi ${wff}\left(\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$