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	$⊢ (A +_{ℎ} B) \cdot_{ih} (C +_{ℎ} D) = (A \cdot_{ih} C) + (B \cdot_{ih} D) + (A \cdot_{ih} D) + (B \cdot_{ih} C)$

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	$⊢ (A \in ℋ \land C \in ℋ \land D \in ℋ) \to A \cdot_{ih} (C +_{ℎ} D) = (A \cdot_{ih} C) + (A \cdot_{ih} D)$
6	1 3 4 5	mp3an	$⊢ A \cdot_{ih} (C +_{ℎ} D) = (A \cdot_{ih} C) + (A \cdot_{ih} D)$
7		his7	$⊢ (B \in ℋ \land C \in ℋ \land D \in ℋ) \to B \cdot_{ih} (C +_{ℎ} D) = (B \cdot_{ih} C) + (B \cdot_{ih} D)$
8	2 3 4 7	mp3an	$⊢ B \cdot_{ih} (C +_{ℎ} D) = (B \cdot_{ih} C) + (B \cdot_{ih} D)$
9	6 8	oveq12i	$⊢ (A \cdot_{ih} (C +_{ℎ} D)) + (B \cdot_{ih} (C +_{ℎ} D)) = (A \cdot_{ih} C) + (A \cdot_{ih} D) + (B \cdot_{ih} C) + (B \cdot_{ih} D)$
10	3 4	hvaddcli	$⊢ C +_{ℎ} D \in ℋ$
11		ax-his2	$⊢ (A \in ℋ \land B \in ℋ \land C +_{ℎ} D \in ℋ) \to (A +_{ℎ} B) \cdot_{ih} (C +_{ℎ} D) = (A \cdot_{ih} (C +_{ℎ} D)) + (B \cdot_{ih} (C +_{ℎ} D))$
12	1 2 10 11	mp3an	$⊢ (A +_{ℎ} B) \cdot_{ih} (C +_{ℎ} D) = (A \cdot_{ih} (C +_{ℎ} D)) + (B \cdot_{ih} (C +_{ℎ} D))$
13	1 3	hicli	$⊢ A \cdot_{ih} C \in ℂ$
14	2 4	hicli	$⊢ B \cdot_{ih} D \in ℂ$
15	1 4	hicli	$⊢ A \cdot_{ih} D \in ℂ$
16	2 3	hicli	$⊢ B \cdot_{ih} C \in ℂ$
17	13 14 15 16	add42i	$⊢ (A \cdot_{ih} C) + (B \cdot_{ih} D) + (A \cdot_{ih} D) + (B \cdot_{ih} C) = (A \cdot_{ih} C) + (A \cdot_{ih} D) + (B \cdot_{ih} C) + (B \cdot_{ih} D)$
18	9 12 17	3eqtr4i	$⊢ (A +_{ℎ} B) \cdot_{ih} (C +_{ℎ} D) = (A \cdot_{ih} C) + (B \cdot_{ih} D) + (A \cdot_{ih} D) + (B \cdot_{ih} C)$

Metamath Proof Explorer