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 31258

Description: Lemma for lnopunii 31260. (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 31217	. . . . . . 7 ⊢ 𝑇: ℋ⟶ ℋ
5	4	ffvelcdmi 7085	. . . . . 6 ⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ)
6	2, 5	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐴) ∈ ℋ
7		lnopunilem.4	. . . . . 6 ⊢ 𝐵 ∈ ℋ
8	4	ffvelcdmi 7085	. . . . . 6 ⊢ (𝐵 ∈ ℋ → (𝑇‘𝐵) ∈ ℋ)
9	7, 8	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐵) ∈ ℋ
10	6, 9	hicli 30329	. . . 4 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)) ∈ ℂ
11	1, 10	mulcli 11220	. . 3 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ
12		reval 15052	. . 3 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ → (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2))
13	11, 12	ax-mp 5	. 2 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
14	2, 7	hicli 30329	. . . . 5 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
15	1, 14	mulcli 11220	. . . 4 ⊢ (𝐶 · (𝐴 ·_ih 𝐵)) ∈ ℂ
16		reval 15052	. . . 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 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘(𝑇‘𝑦)))
20		fveq2 6891	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘𝑥) = (norm_ℎ‘𝑦))
21	19, 20	eqeq12d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)))
22	21	cbvralvw 3234	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ ℋ (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦))
23	18, 22	mpbi 229	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)
24		oveq1 7415	. . . . . . . . . . . . . 14 ⊢ ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2))
25	4	ffvelcdmi 7085	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ)
26		normsq 30382	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇‘𝑦) ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
28		normsq 30382	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘𝑦)↑2) = (𝑦 ·_ih 𝑦))
29	27, 28	eqeq12d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℋ → (((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2) ↔ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
30	24, 29	imbitrid 243	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
31	30	ralimia 3080	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦))
32	23, 31	ax-mp 5	. . . . . . . . . . 11 ⊢ ∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)
33		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → (𝑇‘𝑦) = (𝑇‘𝐴))
34	33, 33	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
35		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
36	35, 35	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → (𝑦 ·_ih 𝑦) = (𝐴 ·_ih 𝐴))
37	34, 36	eqeq12d 2748	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
38	37	rspcv 3608	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
39	2, 32, 38	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)
40	39	oveq2i 7419	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
41	40	oveq2i 7419	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) = (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
42		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → (𝑇‘𝑦) = (𝑇‘𝐵))
43	42, 42	oveq12d 7426	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
44		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
45	44, 44	oveq12d 7426	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → (𝑦 ·_ih 𝑦) = (𝐵 ·_ih 𝐵))
46	43, 45	eqeq12d 2748	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
47	46	rspcv 3608	. . . . . . . . 9 ⊢ (𝐵 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
48	7, 32, 47	mp2 9	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)
49	41, 48	oveq12i 7420	. . . . . . 7 ⊢ ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵))
50	49	oveq1i 7418	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))))
51	1	cjcli 15115	. . . . . . . . . 10 ⊢ (∗‘𝐶) ∈ ℂ
52	6, 6	hicli 30329	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) ∈ ℂ
53	51, 52	mulcli 11220	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) ∈ ℂ
54	1, 53	mulcli 11220	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) ∈ ℂ
55	9, 9	hicli 30329	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) ∈ ℂ
56	11	cjcli 15115	. . . . . . . 8 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) ∈ ℂ
57	54, 55, 11, 56	add42i 11438	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
58	2, 2	hicli 30329	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℂ
59	51, 58	mulcli 11220	. . . . . . . . . 10 ⊢ ((∗‘𝐶) · (𝐴 ·_ih 𝐴)) ∈ ℂ
60	1, 59	mulcli 11220	. . . . . . . . 9 ⊢ (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) ∈ ℂ
61	7, 7	hicli 30329	. . . . . . . . 9 ⊢ (𝐵 ·_ih 𝐵) ∈ ℂ
62	15	cjcli 15115	. . . . . . . . 9 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) ∈ ℂ
63	60, 61, 15, 62	add42i 11438	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
64	1, 2	hvmulcli 30262	. . . . . . . . . . . 12 ⊢ (𝐶 ·_ℎ 𝐴) ∈ ℋ
65	64, 7	hvaddcli 30266	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ
66		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑇‘𝑦) = (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
67	66, 66	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
68		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → 𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
69	68, 68	oveq12d 7426	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑦 ·_ih 𝑦) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
70	67, 69	eqeq12d 2748	. . . . . . . . . . . 12 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
71	70	rspcv 3608	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
72	65, 32, 71	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
73		ax-his2 30331	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
74	64, 7, 65, 73	mp3an 1461	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
75		ax-his3 30332	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
76	1, 2, 65, 75	mp3an 1461	. . . . . . . . . . . 12 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
77		his7 30338	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)))
78	2, 64, 7, 77	mp3an 1461	. . . . . . . . . . . . . 14 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵))
79		his5 30334	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
80	1, 2, 2, 79	mp3an 1461	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
81	80	oveq1i 7418	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
82	78, 81	eqtri 2760	. . . . . . . . . . . . 13 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
83	82	oveq2i 7419	. . . . . . . . . . . 12 ⊢ (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵)))
84	1, 59, 14	adddii 11225	. . . . . . . . . . . 12 ⊢ (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
85	76, 83, 84	3eqtri 2764	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
86		his7 30338	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)))
87	7, 64, 7, 86	mp3an 1461	. . . . . . . . . . . 12 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵))
88		his5 30334	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴)))
89	1, 7, 2, 88	mp3an 1461	. . . . . . . . . . . . . 14 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
90	1, 14	cjmuli 15135	. . . . . . . . . . . . . . 15 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
91	7, 2	his1i 30348	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ·_ih 𝐴) = (∗‘(𝐴 ·_ih 𝐵))
92	91	oveq2i 7419	. . . . . . . . . . . . . . 15 ⊢ ((∗‘𝐶) · (𝐵 ·_ih 𝐴)) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
93	90, 92	eqtr4i 2763	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
94	89, 93	eqtr4i 2763	. . . . . . . . . . . . 13 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))
95	94	oveq1i 7418	. . . . . . . . . . . 12 ⊢ ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
96	87, 95	eqtri 2760	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
97	85, 96	oveq12i 7420	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
98	72, 74, 97	3eqtrri 2765	. . . . . . . . 9 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
99	3	lnopli 31216	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
100	1, 2, 7, 99	mp3an 1461	. . . . . . . . . . 11 ⊢ (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))
101	100, 100	oveq12i 7420	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
102	1, 6	hvmulcli 30262	. . . . . . . . . . 11 ⊢ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ
103	102, 9	hvaddcli 30266	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ
104		ax-his2 30331	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
105	102, 9, 103, 104	mp3an 1461	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
106	101, 105	eqtri 2760	. . . . . . . . 9 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
107		ax-his3 30332	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
108	1, 6, 103, 107	mp3an 1461	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
109		his7 30338	. . . . . . . . . . . . . 14 ⊢ (((𝑇‘𝐴) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
110	6, 102, 9, 109	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
111		his5 30334	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))))
112	1, 6, 6, 111	mp3an 1461	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
113	112	oveq1i 7418	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
114	110, 113	eqtri 2760	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
115	114	oveq2i 7419	. . . . . . . . . . 11 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
116	1, 53, 10	adddii 11225	. . . . . . . . . . 11 ⊢ (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
117	108, 115, 116	3eqtri 2764	. . . . . . . . . 10 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
118		his7 30338	. . . . . . . . . . . 12 ⊢ (((𝑇‘𝐵) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
119	9, 102, 9, 118	mp3an 1461	. . . . . . . . . . 11 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
120		his5 30334	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐵) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))))
121	1, 9, 6, 120	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
122	1, 10	cjmuli 15135	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
123	9, 6	his1i 30348	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)) = (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
124	123	oveq2i 7419	. . . . . . . . . . . . . 14 ⊢ ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
125	122, 124	eqtr4i 2763	. . . . . . . . . . . . 13 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
126	121, 125	eqtr4i 2763	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
127	126	oveq1i 7418	. . . . . . . . . . 11 ⊢ (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
128	119, 127	eqtri 2760	. . . . . . . . . 10 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
129	117, 128	oveq12i 7420	. . . . . . . . 9 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
130	98, 106, 129	3eqtrri 2765	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
131	63, 130	eqtr4i 2763	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
132	57, 131	eqtr4i 2763	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
133	50, 132	eqtr3i 2762	. . . . 5 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
134	60, 61	addcli 11219	. . . . . 6 ⊢ ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) ∈ ℂ
135	11, 56	addcli 11219	. . . . . 6 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) ∈ ℂ
136	15, 62	addcli 11219	. . . . . 6 ⊢ ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) ∈ ℂ
137	134, 135, 136	addcani 11406	. . . . 5 ⊢ ((((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) ↔ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) = ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
138	133, 137	mpbi 229	. . . 4 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) = ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))
139	138	oveq1i 7418	. . 3 ⊢ (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2) = (((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) / 2)
140	17, 139	eqtr4i 2763	. 2 ⊢ (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
141	13, 140	eqtr4i 2763	1 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵)))

Colors of variables: wff setvar class

Syntax hints: = wceq 1541 ∈ wcel 2106 ∀wral 3061 ‘cfv 6543 (class class class)co 7408 ℂcc 11107 + caddc 11112 · cmul 11114 / cdiv 11870 2c2 12266 ↑cexp 14026 ∗ccj 15042 ℜcre 15043 ℋchba 30167 +_ℎ cva 30168 ·_ℎ csm 30169 ·_ih csp 30170 norm_ℎcno 30171 LinOpclo 30195

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187 ax-hilex 30247 ax-hfvadd 30248 ax-hv0cl 30251 ax-hfvmul 30253 ax-hvmul0 30258 ax-hfi 30327 ax-his1 30330 ax-his2 30331 ax-his3 30332 ax-his4 30333

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7855 df-2nd 7975 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-rdg 8409 df-er 8702 df-map 8821 df-en 8939 df-dom 8940 df-sdom 8941 df-sup 9436 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11445 df-neg 11446 df-div 11871 df-nn 12212 df-2 12274 df-3 12275 df-n0 12472 df-z 12558 df-uz 12822 df-rp 12974 df-seq 13966 df-exp 14027 df-cj 15045 df-re 15046 df-im 15047 df-sqrt 15181 df-hnorm 30216 df-lnop 31089

This theorem is referenced by: lnopunilem2 31259

W3C validator