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 \mathscr{H}$$
	normlem8.2	$$⊢B\in \mathscr{H}$$
	normlem8.3	$$⊢C\in \mathscr{H}$$
	normlem8.4	$$⊢D\in \mathscr{H}$$
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 \mathscr{H}$$
2		normlem8.2	$$⊢B\in \mathscr{H}$$
3		normlem8.3	$$⊢C\in \mathscr{H}$$
4		normlem8.4	$$⊢D\in \mathscr{H}$$
5		his7	$$⊢\left(A\in \mathscr{H}\wedge C\in \mathscr{H}\wedge D\in \mathscr{H}\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 \mathscr{H}\wedge C\in \mathscr{H}\wedge D\in \mathscr{H}\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 \mathscr{H}$$
11		ax-his2	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\wedge C{+}_{ℎ}D\in \mathscr{H}\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)$$