lnopunilem1 - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > lnopunilem1		Structured version Visualization version GIF version

Theorem lnopunilem1 29568

Description: Lemma for lnopunii 29570. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
lnopunilem.1	⊢ 𝑇 ∈ LinOp
lnopunilem.2	⊢ ∀𝑥 ∈ ℋ (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥)
lnopunilem.3	⊢ 𝐴 ∈ ℋ
lnopunilem.4	⊢ 𝐵 ∈ ℋ
lnopunilem1.5	⊢ 𝐶 ∈ ℂ

**Assertion**
Ref	Expression
lnopunilem1	⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵)))

Distinct variable group: 𝑥,𝑇 Allowed substitution hints: 𝐴(𝑥) 𝐵(𝑥) 𝐶(𝑥)

Proof of Theorem lnopunilem1 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lnopunilem1.5	. . . 4 ⊢ 𝐶 ∈ ℂ
2		lnopunilem.3	. . . . . 6 ⊢ 𝐴 ∈ ℋ
3		lnopunilem.1	. . . . . . . 8 ⊢ 𝑇 ∈ LinOp
4	3	lnopfi 29527	. . . . . . 7 ⊢ 𝑇: ℋ⟶ ℋ
5	4	ffvelrni 6675	. . . . . 6 ⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ)
6	2, 5	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐴) ∈ ℋ
7		lnopunilem.4	. . . . . 6 ⊢ 𝐵 ∈ ℋ
8	4	ffvelrni 6675	. . . . . 6 ⊢ (𝐵 ∈ ℋ → (𝑇‘𝐵) ∈ ℋ)
9	7, 8	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐵) ∈ ℋ
10	6, 9	hicli 28637	. . . 4 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)) ∈ ℂ
11	1, 10	mulcli 10447	. . 3 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ
12		reval 14326	. . 3 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ → (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2))
13	11, 12	ax-mp 5	. 2 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
14	2, 7	hicli 28637	. . . . 5 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
15	1, 14	mulcli 10447	. . . 4 ⊢ (𝐶 · (𝐴 ·_ih 𝐵)) ∈ ℂ
16		reval 14326	. . . 4 ⊢ ((𝐶 · (𝐴 ·_ih 𝐵)) ∈ ℂ → (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵))) = (((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) / 2))
17	15, 16	ax-mp 5	. . 3 ⊢ (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵))) = (((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) / 2)
18		lnopunilem.2	. . . . . . . . . . . . 13 ⊢ ∀𝑥 ∈ ℋ (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥)
19		2fveq3 6504	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘(𝑇‘𝑦)))
20		fveq2 6499	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘𝑥) = (norm_ℎ‘𝑦))
21	19, 20	eqeq12d 2793	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)))
22	21	cbvralv 3383	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ ℋ (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦))
23	18, 22	mpbi 222	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)
24		oveq1 6983	. . . . . . . . . . . . . 14 ⊢ ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2))
25	4	ffvelrni 6675	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ)
26		normsq 28690	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇‘𝑦) ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
28		normsq 28690	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘𝑦)↑2) = (𝑦 ·_ih 𝑦))
29	27, 28	eqeq12d 2793	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℋ → (((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2) ↔ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
30	24, 29	syl5ib 236	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
31	30	ralimia 3108	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦))
32	23, 31	ax-mp 5	. . . . . . . . . . 11 ⊢ ∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)
33		fveq2 6499	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → (𝑇‘𝑦) = (𝑇‘𝐴))
34	33, 33	oveq12d 6994	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
35		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
36	35, 35	oveq12d 6994	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → (𝑦 ·_ih 𝑦) = (𝐴 ·_ih 𝐴))
37	34, 36	eqeq12d 2793	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
38	37	rspcv 3531	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
39	2, 32, 38	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)
40	39	oveq2i 6987	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
41	40	oveq2i 6987	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) = (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
42		fveq2 6499	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → (𝑇‘𝑦) = (𝑇‘𝐵))
43	42, 42	oveq12d 6994	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
44		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
45	44, 44	oveq12d 6994	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → (𝑦 ·_ih 𝑦) = (𝐵 ·_ih 𝐵))
46	43, 45	eqeq12d 2793	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
47	46	rspcv 3531	. . . . . . . . 9 ⊢ (𝐵 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
48	7, 32, 47	mp2 9	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)
49	41, 48	oveq12i 6988	. . . . . . 7 ⊢ ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵))
50	49	oveq1i 6986	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))))
51	1	cjcli 14389	. . . . . . . . . 10 ⊢ (∗‘𝐶) ∈ ℂ
52	6, 6	hicli 28637	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) ∈ ℂ
53	51, 52	mulcli 10447	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) ∈ ℂ
54	1, 53	mulcli 10447	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) ∈ ℂ
55	9, 9	hicli 28637	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) ∈ ℂ
56	11	cjcli 14389	. . . . . . . 8 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) ∈ ℂ
57	54, 55, 11, 56	add42i 10665	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
58	2, 2	hicli 28637	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℂ
59	51, 58	mulcli 10447	. . . . . . . . . 10 ⊢ ((∗‘𝐶) · (𝐴 ·_ih 𝐴)) ∈ ℂ
60	1, 59	mulcli 10447	. . . . . . . . 9 ⊢ (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) ∈ ℂ
61	7, 7	hicli 28637	. . . . . . . . 9 ⊢ (𝐵 ·_ih 𝐵) ∈ ℂ
62	15	cjcli 14389	. . . . . . . . 9 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) ∈ ℂ
63	60, 61, 15, 62	add42i 10665	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
64	1, 2	hvmulcli 28570	. . . . . . . . . . . 12 ⊢ (𝐶 ·_ℎ 𝐴) ∈ ℋ
65	64, 7	hvaddcli 28574	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ
66		fveq2 6499	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑇‘𝑦) = (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
67	66, 66	oveq12d 6994	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
68		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → 𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
69	68, 68	oveq12d 6994	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑦 ·_ih 𝑦) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
70	67, 69	eqeq12d 2793	. . . . . . . . . . . 12 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
71	70	rspcv 3531	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
72	65, 32, 71	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
73		ax-his2 28639	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
74	64, 7, 65, 73	mp3an 1440	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
75		ax-his3 28640	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
76	1, 2, 65, 75	mp3an 1440	. . . . . . . . . . . 12 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
77		his7 28646	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)))
78	2, 64, 7, 77	mp3an 1440	. . . . . . . . . . . . . 14 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵))
79		his5 28642	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
80	1, 2, 2, 79	mp3an 1440	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
81	80	oveq1i 6986	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
82	78, 81	eqtri 2802	. . . . . . . . . . . . 13 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
83	82	oveq2i 6987	. . . . . . . . . . . 12 ⊢ (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵)))
84	1, 59, 14	adddii 10452	. . . . . . . . . . . 12 ⊢ (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
85	76, 83, 84	3eqtri 2806	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
86		his7 28646	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)))
87	7, 64, 7, 86	mp3an 1440	. . . . . . . . . . . 12 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵))
88		his5 28642	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴)))
89	1, 7, 2, 88	mp3an 1440	. . . . . . . . . . . . . 14 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
90	1, 14	cjmuli 14409	. . . . . . . . . . . . . . 15 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
91	7, 2	his1i 28656	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ·_ih 𝐴) = (∗‘(𝐴 ·_ih 𝐵))
92	91	oveq2i 6987	. . . . . . . . . . . . . . 15 ⊢ ((∗‘𝐶) · (𝐵 ·_ih 𝐴)) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
93	90, 92	eqtr4i 2805	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
94	89, 93	eqtr4i 2805	. . . . . . . . . . . . 13 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))
95	94	oveq1i 6986	. . . . . . . . . . . 12 ⊢ ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
96	87, 95	eqtri 2802	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
97	85, 96	oveq12i 6988	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
98	72, 74, 97	3eqtrri 2807	. . . . . . . . 9 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
99	3	lnopli 29526	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
100	1, 2, 7, 99	mp3an 1440	. . . . . . . . . . 11 ⊢ (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))
101	100, 100	oveq12i 6988	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
102	1, 6	hvmulcli 28570	. . . . . . . . . . 11 ⊢ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ
103	102, 9	hvaddcli 28574	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ
104		ax-his2 28639	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
105	102, 9, 103, 104	mp3an 1440	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
106	101, 105	eqtri 2802	. . . . . . . . 9 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
107		ax-his3 28640	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
108	1, 6, 103, 107	mp3an 1440	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
109		his7 28646	. . . . . . . . . . . . . 14 ⊢ (((𝑇‘𝐴) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
110	6, 102, 9, 109	mp3an 1440	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
111		his5 28642	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))))
112	1, 6, 6, 111	mp3an 1440	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
113	112	oveq1i 6986	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
114	110, 113	eqtri 2802	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
115	114	oveq2i 6987	. . . . . . . . . . 11 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
116	1, 53, 10	adddii 10452	. . . . . . . . . . 11 ⊢ (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
117	108, 115, 116	3eqtri 2806	. . . . . . . . . 10 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
118		his7 28646	. . . . . . . . . . . 12 ⊢ (((𝑇‘𝐵) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
119	9, 102, 9, 118	mp3an 1440	. . . . . . . . . . 11 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
120		his5 28642	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐵) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))))
121	1, 9, 6, 120	mp3an 1440	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
122	1, 10	cjmuli 14409	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
123	9, 6	his1i 28656	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)) = (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
124	123	oveq2i 6987	. . . . . . . . . . . . . 14 ⊢ ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
125	122, 124	eqtr4i 2805	. . . . . . . . . . . . 13 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
126	121, 125	eqtr4i 2805	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
127	126	oveq1i 6986	. . . . . . . . . . 11 ⊢ (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
128	119, 127	eqtri 2802	. . . . . . . . . 10 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
129	117, 128	oveq12i 6988	. . . . . . . . 9 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
130	98, 106, 129	3eqtrri 2807	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
131	63, 130	eqtr4i 2805	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
132	57, 131	eqtr4i 2805	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
133	50, 132	eqtr3i 2804	. . . . 5 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
134	60, 61	addcli 10446	. . . . . 6 ⊢ ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) ∈ ℂ
135	11, 56	addcli 10446	. . . . . 6 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) ∈ ℂ
136	15, 62	addcli 10446	. . . . . 6 ⊢ ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) ∈ ℂ
137	134, 135, 136	addcani 10633	. . . . 5 ⊢ ((((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) ↔ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) = ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
138	133, 137	mpbi 222	. . . 4 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) = ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))
139	138	oveq1i 6986	. . 3 ⊢ (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2) = (((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) / 2)
140	17, 139	eqtr4i 2805	. 2 ⊢ (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
141	13, 140	eqtr4i 2805	1 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵)))

Colors of variables: wff setvar class

Syntax hints: = wceq 1507 ∈ wcel 2050 ∀wral 3088 ‘cfv 6188 (class class class)co 6976 ℂcc 10333 + caddc 10338 · cmul 10340 / cdiv 11098 2c2 11495 ↑cexp 13244 ∗ccj 14316 ℜcre 14317 ℋchba 28475 +_ℎ cva 28476 ·_ℎ csm 28477 ·_ih csp 28478 norm_ℎcno 28479 LinOpclo 28503

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412 ax-pre-sup 10413 ax-hilex 28555 ax-hfvadd 28556 ax-hv0cl 28559 ax-hfvmul 28561 ax-hvmul0 28566 ax-hfi 28635 ax-his1 28638 ax-his2 28639 ax-his3 28640 ax-his4 28641

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-om 7397 df-2nd 7502 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-er 8089 df-map 8208 df-en 8307 df-dom 8308 df-sdom 8309 df-sup 8701 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-div 11099 df-nn 11440 df-2 11503 df-3 11504 df-n0 11708 df-z 11794 df-uz 12059 df-rp 12205 df-seq 13185 df-exp 13245 df-cj 14319 df-re 14320 df-im 14321 df-sqrt 14455 df-hnorm 28524 df-lnop 29399

This theorem is referenced by: lnopunilem2 29569

W3C validator