# Metamath Proof Explorer

## Theorem normlem8

Description: Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005) (New usage is discouraged.)

Ref Expression
Hypotheses normlem8.1 ${⊢}{A}\in ℋ$
normlem8.2 ${⊢}{B}\in ℋ$
normlem8.3 ${⊢}{C}\in ℋ$
normlem8.4 ${⊢}{D}\in ℋ$
Assertion normlem8 ${⊢}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$

### Proof

Step Hyp Ref Expression
1 normlem8.1 ${⊢}{A}\in ℋ$
2 normlem8.2 ${⊢}{B}\in ℋ$
3 normlem8.3 ${⊢}{C}\in ℋ$
4 normlem8.4 ${⊢}{D}\in ℋ$
5 his7 ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\wedge {D}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
6 1 3 4 5 mp3an ${⊢}{A}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)$
7 his7 ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {D}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({B}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
8 2 3 4 7 mp3an ${⊢}{B}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({B}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
9 6 8 oveq12i ${⊢}\left({A}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)\right)+\left({B}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
10 3 4 hvaddcli ${⊢}{C}{+}_{ℎ}{D}\in ℋ$
11 ax-his2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}{+}_{ℎ}{D}\in ℋ\right)\to \left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)\right)+\left({B}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)\right)$
12 1 2 10 11 mp3an ${⊢}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)\right)+\left({B}{\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)\right)$
13 1 3 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
14 2 4 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{D}\in ℂ$
15 1 4 hicli ${⊢}{A}{\cdot }_{\mathrm{ih}}{D}\in ℂ$
16 2 3 hicli ${⊢}{B}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
17 13 14 15 16 add42i ${⊢}\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)$
18 9 12 17 3eqtr4i ${⊢}\left({A}{+}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}\left({C}{+}_{ℎ}{D}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left({B}{\cdot }_{\mathrm{ih}}{D}\right)+\left({A}{\cdot }_{\mathrm{ih}}{D}\right)+\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$