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

 Description: Lemma for cnlnadji 29862. 𝐹 is linear. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
cnlnadjlem.3 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
cnlnadjlem.4 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
cnlnadjlem.5 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
Assertion
Ref Expression
Distinct variable groups:   𝑣,𝑔,𝑤,𝑦   𝑤,𝐹   𝑇,𝑔,𝑣,𝑤,𝑦   𝑣,𝐺,𝑤
Allowed substitution hints:   𝐵(𝑦,𝑤,𝑣,𝑔)   𝐹(𝑦,𝑣,𝑔)   𝐺(𝑦,𝑔)

Dummy variables 𝑓 𝑧 𝑡 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnlnadjlem.5 . . 3 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
2 cnlnadjlem.1 . . . 4 𝑇 ∈ LinOp
3 cnlnadjlem.2 . . . 4 𝑇 ∈ ContOp
4 cnlnadjlem.3 . . . 4 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
5 cnlnadjlem.4 . . . 4 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
62, 3, 4, 5cnlnadjlem3 29855 . . 3 (𝑦 ∈ ℋ → 𝐵 ∈ ℋ)
71, 6fmpti 6867 . 2 𝐹: ℋ⟶ ℋ
82lnopfi 29755 . . . . . . . . . 10 𝑇: ℋ⟶ ℋ
98ffvelrni 6841 . . . . . . . . 9 (𝑡 ∈ ℋ → (𝑇𝑡) ∈ ℋ)
109adantl 485 . . . . . . . 8 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑇𝑡) ∈ ℋ)
11 hvmulcl 28799 . . . . . . . . 9 ((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) → (𝑥 · 𝑓) ∈ ℋ)
1211ad2antrr 725 . . . . . . . 8 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑥 · 𝑓) ∈ ℋ)
13 simplr 768 . . . . . . . 8 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → 𝑧 ∈ ℋ)
14 his7 28876 . . . . . . . 8 (((𝑇𝑡) ∈ ℋ ∧ (𝑥 · 𝑓) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇𝑡) ·ih ((𝑥 · 𝑓) + 𝑧)) = (((𝑇𝑡) ·ih (𝑥 · 𝑓)) + ((𝑇𝑡) ·ih 𝑧)))
1510, 12, 13, 14syl3anc 1368 . . . . . . 7 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih ((𝑥 · 𝑓) + 𝑧)) = (((𝑇𝑡) ·ih (𝑥 · 𝑓)) + ((𝑇𝑡) ·ih 𝑧)))
16 hvaddcl 28798 . . . . . . . . 9 (((𝑥 · 𝑓) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 · 𝑓) + 𝑧) ∈ ℋ)
1711, 16sylan 583 . . . . . . . 8 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥 · 𝑓) + 𝑧) ∈ ℋ)
182, 3, 4, 5, 1cnlnadjlem5 29857 . . . . . . . 8 ((((𝑥 · 𝑓) + 𝑧) ∈ ℋ ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih ((𝑥 · 𝑓) + 𝑧)) = (𝑡 ·ih (𝐹‘((𝑥 · 𝑓) + 𝑧))))
1917, 18sylan 583 . . . . . . 7 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih ((𝑥 · 𝑓) + 𝑧)) = (𝑡 ·ih (𝐹‘((𝑥 · 𝑓) + 𝑧))))
20 simpll 766 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → 𝑥 ∈ ℂ)
219adantl 485 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑇𝑡) ∈ ℋ)
22 simplr 768 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → 𝑓 ∈ ℋ)
23 his5 28872 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ (𝑇𝑡) ∈ ℋ ∧ 𝑓 ∈ ℋ) → ((𝑇𝑡) ·ih (𝑥 · 𝑓)) = ((∗‘𝑥) · ((𝑇𝑡) ·ih 𝑓)))
2420, 21, 22, 23syl3anc 1368 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih (𝑥 · 𝑓)) = ((∗‘𝑥) · ((𝑇𝑡) ·ih 𝑓)))
25 simpr 488 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → 𝑡 ∈ ℋ)
262, 3, 4, 5, 1cnlnadjlem4 29856 . . . . . . . . . . . . . 14 (𝑓 ∈ ℋ → (𝐹𝑓) ∈ ℋ)
2726ad2antlr 726 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝐹𝑓) ∈ ℋ)
28 his5 28872 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ 𝑡 ∈ ℋ ∧ (𝐹𝑓) ∈ ℋ) → (𝑡 ·ih (𝑥 · (𝐹𝑓))) = ((∗‘𝑥) · (𝑡 ·ih (𝐹𝑓))))
2920, 25, 27, 28syl3anc 1368 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑡 ·ih (𝑥 · (𝐹𝑓))) = ((∗‘𝑥) · (𝑡 ·ih (𝐹𝑓))))
302, 3, 4, 5, 1cnlnadjlem5 29857 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℋ ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih 𝑓) = (𝑡 ·ih (𝐹𝑓)))
3130adantll 713 . . . . . . . . . . . . 13 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih 𝑓) = (𝑡 ·ih (𝐹𝑓)))
3231oveq2d 7165 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((∗‘𝑥) · ((𝑇𝑡) ·ih 𝑓)) = ((∗‘𝑥) · (𝑡 ·ih (𝐹𝑓))))
3329, 32eqtr4d 2862 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑡 ·ih (𝑥 · (𝐹𝑓))) = ((∗‘𝑥) · ((𝑇𝑡) ·ih 𝑓)))
3424, 33eqtr4d 2862 . . . . . . . . . 10 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih (𝑥 · 𝑓)) = (𝑡 ·ih (𝑥 · (𝐹𝑓))))
3534adantlr 714 . . . . . . . . 9 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih (𝑥 · 𝑓)) = (𝑡 ·ih (𝑥 · (𝐹𝑓))))
362, 3, 4, 5, 1cnlnadjlem5 29857 . . . . . . . . . 10 ((𝑧 ∈ ℋ ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih 𝑧) = (𝑡 ·ih (𝐹𝑧)))
3736adantll 713 . . . . . . . . 9 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → ((𝑇𝑡) ·ih 𝑧) = (𝑡 ·ih (𝐹𝑧)))
3835, 37oveq12d 7167 . . . . . . . 8 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (((𝑇𝑡) ·ih (𝑥 · 𝑓)) + ((𝑇𝑡) ·ih 𝑧)) = ((𝑡 ·ih (𝑥 · (𝐹𝑓))) + (𝑡 ·ih (𝐹𝑧))))
39 simpr 488 . . . . . . . . 9 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → 𝑡 ∈ ℋ)
40 hvmulcl 28799 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ (𝐹𝑓) ∈ ℋ) → (𝑥 · (𝐹𝑓)) ∈ ℋ)
4126, 40sylan2 595 . . . . . . . . . 10 ((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) → (𝑥 · (𝐹𝑓)) ∈ ℋ)
4241ad2antrr 725 . . . . . . . . 9 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑥 · (𝐹𝑓)) ∈ ℋ)
432, 3, 4, 5, 1cnlnadjlem4 29856 . . . . . . . . . 10 (𝑧 ∈ ℋ → (𝐹𝑧) ∈ ℋ)
4443ad2antlr 726 . . . . . . . . 9 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝐹𝑧) ∈ ℋ)
45 his7 28876 . . . . . . . . 9 ((𝑡 ∈ ℋ ∧ (𝑥 · (𝐹𝑓)) ∈ ℋ ∧ (𝐹𝑧) ∈ ℋ) → (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))) = ((𝑡 ·ih (𝑥 · (𝐹𝑓))) + (𝑡 ·ih (𝐹𝑧))))
4639, 42, 44, 45syl3anc 1368 . . . . . . . 8 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))) = ((𝑡 ·ih (𝑥 · (𝐹𝑓))) + (𝑡 ·ih (𝐹𝑧))))
4738, 46eqtr4d 2862 . . . . . . 7 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (((𝑇𝑡) ·ih (𝑥 · 𝑓)) + ((𝑇𝑡) ·ih 𝑧)) = (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))))
4815, 19, 473eqtr3d 2867 . . . . . 6 ((((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ 𝑡 ∈ ℋ) → (𝑡 ·ih (𝐹‘((𝑥 · 𝑓) + 𝑧))) = (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))))
4948ralrimiva 3177 . . . . 5 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ∀𝑡 ∈ ℋ (𝑡 ·ih (𝐹‘((𝑥 · 𝑓) + 𝑧))) = (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))))
502, 3, 4, 5, 1cnlnadjlem4 29856 . . . . . . 7 (((𝑥 · 𝑓) + 𝑧) ∈ ℋ → (𝐹‘((𝑥 · 𝑓) + 𝑧)) ∈ ℋ)
5117, 50syl 17 . . . . . 6 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝐹‘((𝑥 · 𝑓) + 𝑧)) ∈ ℋ)
52 hvaddcl 28798 . . . . . . 7 (((𝑥 · (𝐹𝑓)) ∈ ℋ ∧ (𝐹𝑧) ∈ ℋ) → ((𝑥 · (𝐹𝑓)) + (𝐹𝑧)) ∈ ℋ)
5341, 43, 52syl2an 598 . . . . . 6 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥 · (𝐹𝑓)) + (𝐹𝑧)) ∈ ℋ)
54 hial2eq2 28893 . . . . . 6 (((𝐹‘((𝑥 · 𝑓) + 𝑧)) ∈ ℋ ∧ ((𝑥 · (𝐹𝑓)) + (𝐹𝑧)) ∈ ℋ) → (∀𝑡 ∈ ℋ (𝑡 ·ih (𝐹‘((𝑥 · 𝑓) + 𝑧))) = (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))) ↔ (𝐹‘((𝑥 · 𝑓) + 𝑧)) = ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))))
5551, 53, 54syl2anc 587 . . . . 5 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (∀𝑡 ∈ ℋ (𝑡 ·ih (𝐹‘((𝑥 · 𝑓) + 𝑧))) = (𝑡 ·ih ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))) ↔ (𝐹‘((𝑥 · 𝑓) + 𝑧)) = ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))))
5649, 55mpbid 235 . . . 4 (((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝐹‘((𝑥 · 𝑓) + 𝑧)) = ((𝑥 · (𝐹𝑓)) + (𝐹𝑧)))
5756ralrimiva 3177 . . 3 ((𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ) → ∀𝑧 ∈ ℋ (𝐹‘((𝑥 · 𝑓) + 𝑧)) = ((𝑥 · (𝐹𝑓)) + (𝐹𝑧)))
5857rgen2 3198 . 2 𝑥 ∈ ℂ ∀𝑓 ∈ ℋ ∀𝑧 ∈ ℋ (𝐹‘((𝑥 · 𝑓) + 𝑧)) = ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))
59 ellnop 29644 . 2 (𝐹 ∈ LinOp ↔ (𝐹: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑓 ∈ ℋ ∀𝑧 ∈ ℋ (𝐹‘((𝑥 · 𝑓) + 𝑧)) = ((𝑥 · (𝐹𝑓)) + (𝐹𝑧))))
607, 58, 59mpbir2an 710 1 𝐹 ∈ LinOp