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 32029

Description: Lemma for lnopunii 32031. (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 31988	. . . . . . 7 ⊢ 𝑇: ℋ⟶ ℋ
5	4	ffvelcdmi 7103	. . . . . 6 ⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ)
6	2, 5	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐴) ∈ ℋ
7		lnopunilem.4	. . . . . 6 ⊢ 𝐵 ∈ ℋ
8	4	ffvelcdmi 7103	. . . . . 6 ⊢ (𝐵 ∈ ℋ → (𝑇‘𝐵) ∈ ℋ)
9	7, 8	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐵) ∈ ℋ
10	6, 9	hicli 31100	. . . 4 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)) ∈ ℂ
11	1, 10	mulcli 11268	. . 3 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ
12		reval 15145	. . 3 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ → (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2))
13	11, 12	ax-mp 5	. 2 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
14	2, 7	hicli 31100	. . . . 5 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
15	1, 14	mulcli 11268	. . . 4 ⊢ (𝐶 · (𝐴 ·_ih 𝐵)) ∈ ℂ
16		reval 15145	. . . 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 6911	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘(𝑇‘𝑦)))
20		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘𝑥) = (norm_ℎ‘𝑦))
21	19, 20	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)))
22	21	cbvralvw 3237	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ ℋ (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦))
23	18, 22	mpbi 230	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)
24		oveq1 7438	. . . . . . . . . . . . . 14 ⊢ ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2))
25	4	ffvelcdmi 7103	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ)
26		normsq 31153	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇‘𝑦) ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
28		normsq 31153	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘𝑦)↑2) = (𝑦 ·_ih 𝑦))
29	27, 28	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℋ → (((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2) ↔ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
30	24, 29	imbitrid 244	. . . . . . . . . . . . 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 6906	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → (𝑇‘𝑦) = (𝑇‘𝐴))
34	33, 33	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
35		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
36	35, 35	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → (𝑦 ·_ih 𝑦) = (𝐴 ·_ih 𝐴))
37	34, 36	eqeq12d 2753	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
38	37	rspcv 3618	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
39	2, 32, 38	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)
40	39	oveq2i 7442	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
41	40	oveq2i 7442	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) = (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
42		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → (𝑇‘𝑦) = (𝑇‘𝐵))
43	42, 42	oveq12d 7449	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
44		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
45	44, 44	oveq12d 7449	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → (𝑦 ·_ih 𝑦) = (𝐵 ·_ih 𝐵))
46	43, 45	eqeq12d 2753	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
47	46	rspcv 3618	. . . . . . . . 9 ⊢ (𝐵 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
48	7, 32, 47	mp2 9	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)
49	41, 48	oveq12i 7443	. . . . . . 7 ⊢ ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵))
50	49	oveq1i 7441	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))))
51	1	cjcli 15208	. . . . . . . . . 10 ⊢ (∗‘𝐶) ∈ ℂ
52	6, 6	hicli 31100	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) ∈ ℂ
53	51, 52	mulcli 11268	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) ∈ ℂ
54	1, 53	mulcli 11268	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) ∈ ℂ
55	9, 9	hicli 31100	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) ∈ ℂ
56	11	cjcli 15208	. . . . . . . 8 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) ∈ ℂ
57	54, 55, 11, 56	add42i 11487	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
58	2, 2	hicli 31100	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℂ
59	51, 58	mulcli 11268	. . . . . . . . . 10 ⊢ ((∗‘𝐶) · (𝐴 ·_ih 𝐴)) ∈ ℂ
60	1, 59	mulcli 11268	. . . . . . . . 9 ⊢ (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) ∈ ℂ
61	7, 7	hicli 31100	. . . . . . . . 9 ⊢ (𝐵 ·_ih 𝐵) ∈ ℂ
62	15	cjcli 15208	. . . . . . . . 9 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) ∈ ℂ
63	60, 61, 15, 62	add42i 11487	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
64	1, 2	hvmulcli 31033	. . . . . . . . . . . 12 ⊢ (𝐶 ·_ℎ 𝐴) ∈ ℋ
65	64, 7	hvaddcli 31037	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ
66		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑇‘𝑦) = (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
67	66, 66	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
68		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → 𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
69	68, 68	oveq12d 7449	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑦 ·_ih 𝑦) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
70	67, 69	eqeq12d 2753	. . . . . . . . . . . 12 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
71	70	rspcv 3618	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
72	65, 32, 71	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
73		ax-his2 31102	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
74	64, 7, 65, 73	mp3an 1463	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
75		ax-his3 31103	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
76	1, 2, 65, 75	mp3an 1463	. . . . . . . . . . . 12 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
77		his7 31109	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)))
78	2, 64, 7, 77	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵))
79		his5 31105	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
80	1, 2, 2, 79	mp3an 1463	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
81	80	oveq1i 7441	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
82	78, 81	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
83	82	oveq2i 7442	. . . . . . . . . . . 12 ⊢ (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵)))
84	1, 59, 14	adddii 11273	. . . . . . . . . . . 12 ⊢ (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
85	76, 83, 84	3eqtri 2769	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
86		his7 31109	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)))
87	7, 64, 7, 86	mp3an 1463	. . . . . . . . . . . 12 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵))
88		his5 31105	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴)))
89	1, 7, 2, 88	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
90	1, 14	cjmuli 15228	. . . . . . . . . . . . . . 15 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
91	7, 2	his1i 31119	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ·_ih 𝐴) = (∗‘(𝐴 ·_ih 𝐵))
92	91	oveq2i 7442	. . . . . . . . . . . . . . 15 ⊢ ((∗‘𝐶) · (𝐵 ·_ih 𝐴)) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
93	90, 92	eqtr4i 2768	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
94	89, 93	eqtr4i 2768	. . . . . . . . . . . . 13 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))
95	94	oveq1i 7441	. . . . . . . . . . . 12 ⊢ ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
96	87, 95	eqtri 2765	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
97	85, 96	oveq12i 7443	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
98	72, 74, 97	3eqtrri 2770	. . . . . . . . 9 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
99	3	lnopli 31987	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
100	1, 2, 7, 99	mp3an 1463	. . . . . . . . . . 11 ⊢ (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))
101	100, 100	oveq12i 7443	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
102	1, 6	hvmulcli 31033	. . . . . . . . . . 11 ⊢ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ
103	102, 9	hvaddcli 31037	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ
104		ax-his2 31102	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
105	102, 9, 103, 104	mp3an 1463	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
106	101, 105	eqtri 2765	. . . . . . . . 9 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
107		ax-his3 31103	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
108	1, 6, 103, 107	mp3an 1463	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
109		his7 31109	. . . . . . . . . . . . . 14 ⊢ (((𝑇‘𝐴) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
110	6, 102, 9, 109	mp3an 1463	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
111		his5 31105	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))))
112	1, 6, 6, 111	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
113	112	oveq1i 7441	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
114	110, 113	eqtri 2765	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
115	114	oveq2i 7442	. . . . . . . . . . 11 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
116	1, 53, 10	adddii 11273	. . . . . . . . . . 11 ⊢ (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
117	108, 115, 116	3eqtri 2769	. . . . . . . . . 10 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
118		his7 31109	. . . . . . . . . . . 12 ⊢ (((𝑇‘𝐵) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
119	9, 102, 9, 118	mp3an 1463	. . . . . . . . . . 11 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
120		his5 31105	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐵) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))))
121	1, 9, 6, 120	mp3an 1463	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
122	1, 10	cjmuli 15228	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
123	9, 6	his1i 31119	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)) = (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
124	123	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
125	122, 124	eqtr4i 2768	. . . . . . . . . . . . 13 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
126	121, 125	eqtr4i 2768	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
127	126	oveq1i 7441	. . . . . . . . . . 11 ⊢ (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
128	119, 127	eqtri 2765	. . . . . . . . . 10 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
129	117, 128	oveq12i 7443	. . . . . . . . 9 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
130	98, 106, 129	3eqtrri 2770	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
131	63, 130	eqtr4i 2768	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
132	57, 131	eqtr4i 2768	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
133	50, 132	eqtr3i 2767	. . . . 5 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
134	60, 61	addcli 11267	. . . . . 6 ⊢ ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) ∈ ℂ
135	11, 56	addcli 11267	. . . . . 6 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) ∈ ℂ
136	15, 62	addcli 11267	. . . . . 6 ⊢ ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) ∈ ℂ
137	134, 135, 136	addcani 11454	. . . . 5 ⊢ ((((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) ↔ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) = ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
138	133, 137	mpbi 230	. . . 4 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) = ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))
139	138	oveq1i 7441	. . 3 ⊢ (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2) = (((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) / 2)
140	17, 139	eqtr4i 2768	. 2 ⊢ (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
141	13, 140	eqtr4i 2768	1 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵)))

Colors of variables: wff setvar class

Syntax hints: = wceq 1540 ∈ wcel 2108 ∀wral 3061 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 + caddc 11158 · cmul 11160 / cdiv 11920 2c2 12321 ↑cexp 14102 ∗ccj 15135 ℜcre 15136 ℋchba 30938 +_ℎ cva 30939 ·_ℎ csm 30940 ·_ih csp 30941 norm_ℎcno 30942 LinOpclo 30966

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-hilex 31018 ax-hfvadd 31019 ax-hv0cl 31022 ax-hfvmul 31024 ax-hvmul0 31029 ax-hfi 31098 ax-his1 31101 ax-his2 31102 ax-his3 31103 ax-his4 31104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-sup 9482 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-z 12614 df-uz 12879 df-rp 13035 df-seq 14043 df-exp 14103 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-hnorm 30987 df-lnop 31860

This theorem is referenced by: lnopunilem2 32030

W3C validator