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 30273

Description: Lemma for lnopunii 30275. (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 30232	. . . . . . 7 ⊢ 𝑇: ℋ⟶ ℋ
5	4	ffvelrni 6942	. . . . . 6 ⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ)
6	2, 5	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐴) ∈ ℋ
7		lnopunilem.4	. . . . . 6 ⊢ 𝐵 ∈ ℋ
8	4	ffvelrni 6942	. . . . . 6 ⊢ (𝐵 ∈ ℋ → (𝑇‘𝐵) ∈ ℋ)
9	7, 8	ax-mp 5	. . . . 5 ⊢ (𝑇‘𝐵) ∈ ℋ
10	6, 9	hicli 29344	. . . 4 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)) ∈ ℂ
11	1, 10	mulcli 10913	. . 3 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ
12		reval 14745	. . 3 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) ∈ ℂ → (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2))
13	11, 12	ax-mp 5	. 2 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
14	2, 7	hicli 29344	. . . . 5 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
15	1, 14	mulcli 10913	. . . 4 ⊢ (𝐶 · (𝐴 ·_ih 𝐵)) ∈ ℂ
16		reval 14745	. . . 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 6761	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘(𝑇‘𝑦)))
20		fveq2 6756	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (norm_ℎ‘𝑥) = (norm_ℎ‘𝑦))
21	19, 20	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)))
22	21	cbvralvw 3372	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ ℋ (norm_ℎ‘(𝑇‘𝑥)) = (norm_ℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦))
23	18, 22	mpbi 229	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦)
24		oveq1 7262	. . . . . . . . . . . . . 14 ⊢ ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2))
25	4	ffvelrni 6942	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ)
26		normsq 29397	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇‘𝑦) ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦))↑2) = ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)))
28		normsq 29397	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘𝑦)↑2) = (𝑦 ·_ih 𝑦))
29	27, 28	eqeq12d 2754	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℋ → (((norm_ℎ‘(𝑇‘𝑦))↑2) = ((norm_ℎ‘𝑦)↑2) ↔ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
30	24, 29	syl5ib 243	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℋ → ((norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)))
31	30	ralimia 3084	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ ℋ (norm_ℎ‘(𝑇‘𝑦)) = (norm_ℎ‘𝑦) → ∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦))
32	23, 31	ax-mp 5	. . . . . . . . . . 11 ⊢ ∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦)
33		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → (𝑇‘𝑦) = (𝑇‘𝐴))
34	33, 33	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
35		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
36	35, 35	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐴 → (𝑦 ·_ih 𝑦) = (𝐴 ·_ih 𝐴))
37	34, 36	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
38	37	rspcv 3547	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)))
39	2, 32, 38	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) = (𝐴 ·_ih 𝐴)
40	39	oveq2i 7266	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
41	40	oveq2i 7266	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) = (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
42		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → (𝑇‘𝑦) = (𝑇‘𝐵))
43	42, 42	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
44		id 22	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵)
45	44, 44	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → (𝑦 ·_ih 𝑦) = (𝐵 ·_ih 𝐵))
46	43, 45	eqeq12d 2754	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
47	46	rspcv 3547	. . . . . . . . 9 ⊢ (𝐵 ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)))
48	7, 32, 47	mp2 9	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) = (𝐵 ·_ih 𝐵)
49	41, 48	oveq12i 7267	. . . . . . 7 ⊢ ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵))
50	49	oveq1i 7265	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))))
51	1	cjcli 14808	. . . . . . . . . 10 ⊢ (∗‘𝐶) ∈ ℂ
52	6, 6	hicli 29344	. . . . . . . . . 10 ⊢ ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)) ∈ ℂ
53	51, 52	mulcli 10913	. . . . . . . . 9 ⊢ ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) ∈ ℂ
54	1, 53	mulcli 10913	. . . . . . . 8 ⊢ (𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) ∈ ℂ
55	9, 9	hicli 29344	. . . . . . . 8 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)) ∈ ℂ
56	11	cjcli 14808	. . . . . . . 8 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) ∈ ℂ
57	54, 55, 11, 56	add42i 11130	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
58	2, 2	hicli 29344	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℂ
59	51, 58	mulcli 10913	. . . . . . . . . 10 ⊢ ((∗‘𝐶) · (𝐴 ·_ih 𝐴)) ∈ ℂ
60	1, 59	mulcli 10913	. . . . . . . . 9 ⊢ (𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) ∈ ℂ
61	7, 7	hicli 29344	. . . . . . . . 9 ⊢ (𝐵 ·_ih 𝐵) ∈ ℂ
62	15	cjcli 14808	. . . . . . . . 9 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) ∈ ℂ
63	60, 61, 15, 62	add42i 11130	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
64	1, 2	hvmulcli 29277	. . . . . . . . . . . 12 ⊢ (𝐶 ·_ℎ 𝐴) ∈ ℋ
65	64, 7	hvaddcli 29281	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ
66		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑇‘𝑦) = (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
67	66, 66	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
68		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → 𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
69	68, 68	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (𝑦 ·_ih 𝑦) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
70	67, 69	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ (𝑦 = ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) → (((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) ↔ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
71	70	rspcv 3547	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ → (∀𝑦 ∈ ℋ ((𝑇‘𝑦) ·_ih (𝑇‘𝑦)) = (𝑦 ·_ih 𝑦) → ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
72	65, 32, 71	mp2 9	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))
73		ax-his2 29346	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
74	64, 7, 65, 73	mp3an 1459	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
75		ax-his3 29347	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵) ∈ ℋ) → ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))))
76	1, 2, 65, 75	mp3an 1459	. . . . . . . . . . . 12 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
77		his7 29353	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)))
78	2, 64, 7, 77	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵))
79		his5 29349	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴)))
80	1, 2, 2, 79	mp3an 1459	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐴 ·_ih 𝐴))
81	80	oveq1i 7265	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐴 ·_ih 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
82	78, 81	eqtri 2766	. . . . . . . . . . . . 13 ⊢ (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))
83	82	oveq2i 7266	. . . . . . . . . . . 12 ⊢ (𝐶 · (𝐴 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵)))
84	1, 59, 14	adddii 10918	. . . . . . . . . . . 12 ⊢ (𝐶 · (((∗‘𝐶) · (𝐴 ·_ih 𝐴)) + (𝐴 ·_ih 𝐵))) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
85	76, 83, 84	3eqtri 2770	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵)))
86		his7 29353	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℋ ∧ (𝐶 ·_ℎ 𝐴) ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)))
87	7, 64, 7, 86	mp3an 1459	. . . . . . . . . . . 12 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵))
88		his5 29349	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴)))
89	1, 7, 2, 88	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
90	1, 14	cjmuli 14828	. . . . . . . . . . . . . . 15 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
91	7, 2	his1i 29363	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ·_ih 𝐴) = (∗‘(𝐴 ·_ih 𝐵))
92	91	oveq2i 7266	. . . . . . . . . . . . . . 15 ⊢ ((∗‘𝐶) · (𝐵 ·_ih 𝐴)) = ((∗‘𝐶) · (∗‘(𝐴 ·_ih 𝐵)))
93	90, 92	eqtr4i 2769	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · (𝐴 ·_ih 𝐵))) = ((∗‘𝐶) · (𝐵 ·_ih 𝐴))
94	89, 93	eqtr4i 2769	. . . . . . . . . . . . 13 ⊢ (𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) = (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))
95	94	oveq1i 7265	. . . . . . . . . . . 12 ⊢ ((𝐵 ·_ih (𝐶 ·_ℎ 𝐴)) + (𝐵 ·_ih 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
96	87, 95	eqtri 2766	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))
97	85, 96	oveq12i 7267	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ 𝐴) ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) + (𝐵 ·_ih ((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
98	72, 74, 97	3eqtrri 2771	. . . . . . . . 9 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵))) = ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)))
99	3	lnopli 30231	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
100	1, 2, 7, 99	mp3an 1459	. . . . . . . . . . 11 ⊢ (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))
101	100, 100	oveq12i 7267	. . . . . . . . . 10 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))
102	1, 6	hvmulcli 29277	. . . . . . . . . . 11 ⊢ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ
103	102, 9	hvaddcli 29281	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ
104		ax-his2 29346	. . . . . . . . . . 11 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
105	102, 9, 103, 104	mp3an 1459	. . . . . . . . . 10 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
106	101, 105	eqtri 2766	. . . . . . . . 9 ⊢ ((𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵)) ·_ih (𝑇‘((𝐶 ·_ℎ 𝐴) +_ℎ 𝐵))) = (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
107		ax-his3 29347	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)) ∈ ℋ) → ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))))
108	1, 6, 103, 107	mp3an 1459	. . . . . . . . . . 11 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))))
109		his7 29353	. . . . . . . . . . . . . 14 ⊢ (((𝑇‘𝐴) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
110	6, 102, 9, 109	mp3an 1459	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
111		his5 29349	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))))
112	1, 6, 6, 111	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))
113	112	oveq1i 7265	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝐴) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
114	110, 113	eqtri 2766	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
115	114	oveq2i 7266	. . . . . . . . . . 11 ⊢ (𝐶 · ((𝑇‘𝐴) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
116	1, 53, 10	adddii 10918	. . . . . . . . . . 11 ⊢ (𝐶 · (((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴))) + ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
117	108, 115, 116	3eqtri 2770	. . . . . . . . . 10 ⊢ ((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
118		his7 29353	. . . . . . . . . . . 12 ⊢ (((𝑇‘𝐵) ∈ ℋ ∧ (𝐶 ·_ℎ (𝑇‘𝐴)) ∈ ℋ ∧ (𝑇‘𝐵) ∈ ℋ) → ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
119	9, 102, 9, 118	mp3an 1459	. . . . . . . . . . 11 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
120		his5 29349	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℂ ∧ (𝑇‘𝐵) ∈ ℋ ∧ (𝑇‘𝐴) ∈ ℋ) → ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))))
121	1, 9, 6, 120	mp3an 1459	. . . . . . . . . . . . 13 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
122	1, 10	cjmuli 14828	. . . . . . . . . . . . . 14 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
123	9, 6	his1i 29363	. . . . . . . . . . . . . . 15 ⊢ ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)) = (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))
124	123	oveq2i 7266	. . . . . . . . . . . . . 14 ⊢ ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴))) = ((∗‘𝐶) · (∗‘((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
125	122, 124	eqtr4i 2769	. . . . . . . . . . . . 13 ⊢ (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = ((∗‘𝐶) · ((𝑇‘𝐵) ·_ih (𝑇‘𝐴)))
126	121, 125	eqtr4i 2769	. . . . . . . . . . . 12 ⊢ ((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) = (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))
127	126	oveq1i 7265	. . . . . . . . . . 11 ⊢ (((𝑇‘𝐵) ·_ih (𝐶 ·_ℎ (𝑇‘𝐴))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
128	119, 127	eqtri 2766	. . . . . . . . . 10 ⊢ ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) = ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))
129	117, 128	oveq12i 7267	. . . . . . . . 9 ⊢ (((𝐶 ·_ℎ (𝑇‘𝐴)) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵))) + ((𝑇‘𝐵) ·_ih ((𝐶 ·_ℎ (𝑇‘𝐴)) +_ℎ (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
130	98, 106, 129	3eqtrri 2771	. . . . . . . 8 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵)))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐶 · (𝐴 ·_ih 𝐵))) + ((∗‘(𝐶 · (𝐴 ·_ih 𝐵))) + (𝐵 ·_ih 𝐵)))
131	63, 130	eqtr4i 2769	. . . . . . 7 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵))))) = (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + (𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))))
132	57, 131	eqtr4i 2769	. . . . . 6 ⊢ (((𝐶 · ((∗‘𝐶) · ((𝑇‘𝐴) ·_ih (𝑇‘𝐴)))) + ((𝑇‘𝐵) ·_ih (𝑇‘𝐵))) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
133	50, 132	eqtr3i 2768	. . . . 5 ⊢ (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))))) = (((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) + ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))))
134	60, 61	addcli 10912	. . . . . 6 ⊢ ((𝐶 · ((∗‘𝐶) · (𝐴 ·_ih 𝐴))) + (𝐵 ·_ih 𝐵)) ∈ ℂ
135	11, 56	addcli 10912	. . . . . 6 ⊢ ((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) ∈ ℂ
136	15, 62	addcli 10912	. . . . . 6 ⊢ ((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) ∈ ℂ
137	134, 135, 136	addcani 11098	. . . . 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 7265	. . 3 ⊢ (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2) = (((𝐶 · (𝐴 ·_ih 𝐵)) + (∗‘(𝐶 · (𝐴 ·_ih 𝐵)))) / 2)
140	17, 139	eqtr4i 2769	. 2 ⊢ (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵))) = (((𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))) + (∗‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵))))) / 2)
141	13, 140	eqtr4i 2769	1 ⊢ (ℜ‘(𝐶 · ((𝑇‘𝐴) ·_ih (𝑇‘𝐵)))) = (ℜ‘(𝐶 · (𝐴 ·_ih 𝐵)))

Colors of variables: wff setvar class

Syntax hints: = wceq 1539 ∈ wcel 2108 ∀wral 3063 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 + caddc 10805 · cmul 10807 / cdiv 11562 2c2 11958 ↑cexp 13710 ∗ccj 14735 ℜcre 14736 ℋchba 29182 +_ℎ cva 29183 ·_ℎ csm 29184 ·_ih csp 29185 norm_ℎcno 29186 LinOpclo 29210

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-hilex 29262 ax-hfvadd 29263 ax-hv0cl 29266 ax-hfvmul 29268 ax-hvmul0 29273 ax-hfi 29342 ax-his1 29345 ax-his2 29346 ax-his3 29347 ax-his4 29348

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-hnorm 29231 df-lnop 30104

This theorem is referenced by: lnopunilem2 30274

W3C validator