Step | Hyp | Ref
| Expression |
1 | | htth.3 |
. . . . . . 7
⊢ 𝐿 = (𝑈 LnOp 𝑈) |
2 | | oveq12 7367 |
. . . . . . . 8
⊢ ((𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) ∧ 𝑈
= if(𝑈 ∈
CHilOLD, 𝑈,
⟨⟨ + , · ⟩, abs⟩)) → (𝑈 LnOp 𝑈) = (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
3 | 2 | anidms 568 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (𝑈 LnOp 𝑈) = (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
4 | 1, 3 | eqtrid 2785 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → 𝐿
= (if(𝑈 ∈
CHilOLD, 𝑈,
⟨⟨ + , · ⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
5 | 4 | eleq2d 2820 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (𝑇 ∈ 𝐿 ↔ 𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)))) |
6 | | htth.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
7 | | fveq2 6843 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (BaseSet‘𝑈) = (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
8 | 6, 7 | eqtrid 2785 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → 𝑋
= (BaseSet‘if(𝑈
∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))) |
9 | | htth.2 |
. . . . . . . . . 10
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
10 | | fveq2 6843 |
. . . . . . . . . 10
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (·𝑖OLD‘𝑈) =
(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
11 | 9, 10 | eqtrid 2785 |
. . . . . . . . 9
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → 𝑃
= (·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
12 | 11 | oveqd 7375 |
. . . . . . . 8
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (𝑥𝑃(𝑇‘𝑦)) = (𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦))) |
13 | 11 | oveqd 7375 |
. . . . . . . 8
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → ((𝑇‘𝑥)𝑃𝑦) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) |
14 | 12, 13 | eqeq12d 2749 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → ((𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦) ↔ (𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦))) |
15 | 8, 14 | raleqbidv 3318 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦) ↔ ∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦))) |
16 | 8, 15 | raleqbidv 3318 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦) ↔ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦))) |
17 | 5, 16 | anbi12d 632 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → ((𝑇 ∈ 𝐿 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) ↔ (𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∧ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)))) |
18 | | htth.4 |
. . . . . 6
⊢ 𝐵 = (𝑈 BLnOp 𝑈) |
19 | | oveq12 7367 |
. . . . . . 7
⊢ ((𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) ∧ 𝑈
= if(𝑈 ∈
CHilOLD, 𝑈,
⟨⟨ + , · ⟩, abs⟩)) → (𝑈 BLnOp 𝑈) = (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) BLnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
20 | 19 | anidms 568 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (𝑈 BLnOp 𝑈) = (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) BLnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
21 | 18, 20 | eqtrid 2785 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → 𝐵
= (if(𝑈 ∈
CHilOLD, 𝑈,
⟨⟨ + , · ⟩, abs⟩) BLnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))) |
22 | 21 | eleq2d 2820 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (𝑇 ∈ 𝐵 ↔ 𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) BLnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)))) |
23 | 17, 22 | imbi12d 345 |
. . 3
⊢ (𝑈 = if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) → (((𝑇 ∈ 𝐿 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) → 𝑇 ∈ 𝐵) ↔ ((𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∧ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) → 𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) BLnOp
if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))))) |
24 | | eqid 2733 |
. . . 4
⊢
(BaseSet‘if(𝑈
∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩)) = (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) |
25 | | eqid 2733 |
. . . 4
⊢
(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) = (·𝑖OLD‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩)) |
26 | | eqid 2733 |
. . . 4
⊢ (if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) = (if(𝑈
∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩) LnOp if(𝑈 ∈
CHilOLD, 𝑈,
⟨⟨ + , · ⟩, abs⟩)) |
27 | | eqid 2733 |
. . . 4
⊢ (if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩) BLnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) = (if(𝑈
∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩) BLnOp if(𝑈
∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩)) |
28 | | eqid 2733 |
. . . 4
⊢
(normCV‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) = (normCV‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) |
29 | | eqid 2733 |
. . . . . 6
⊢
⟨⟨ + , · ⟩, abs⟩ = ⟨⟨ + , ·
⟩, abs⟩ |
30 | 29 | cnchl 29900 |
. . . . 5
⊢
⟨⟨ + , · ⟩, abs⟩ ∈
CHilOLD |
31 | 30 | elimel 4556 |
. . . 4
⊢ if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩) ∈ CHilOLD |
32 | | simpl 484 |
. . . 4
⊢ ((𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∧ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) → 𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) LnOp
if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))) |
33 | | simpr 486 |
. . . . 5
⊢ ((𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∧ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) → ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))∀𝑦 ∈
(BaseSet‘if(𝑈 ∈
CHilOLD, 𝑈, ⟨⟨ +
, · ⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) |
34 | | oveq1 7365 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = (𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦))) |
35 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑇‘𝑥) = (𝑇‘𝑢)) |
36 | 35 | oveq1d 7373 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) |
37 | 34, 36 | eqeq12d 2749 |
. . . . . 6
⊢ (𝑥 = 𝑢 → ((𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦) ↔ (𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦))) |
38 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → (𝑇‘𝑦) = (𝑇‘𝑣)) |
39 | 38 | oveq2d 7374 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → (𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = (𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑣))) |
40 | | oveq2 7366 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑣)) |
41 | 39, 40 | eqeq12d 2749 |
. . . . . 6
⊢ (𝑦 = 𝑣 → ((𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦) ↔ (𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑣)) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑣))) |
42 | 37, 41 | cbvral2vw 3226 |
. . . . 5
⊢
(∀𝑥 ∈
(BaseSet‘if(𝑈 ∈
CHilOLD, 𝑈,
⟨⟨ + , · ⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦) ↔ ∀𝑢 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))∀𝑣 ∈
(BaseSet‘if(𝑈 ∈
CHilOLD, 𝑈, ⟨⟨ +
, · ⟩, abs⟩))(𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑣)) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑣)) |
43 | 33, 42 | sylib 217 |
. . . 4
⊢ ((𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∧ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) → ∀𝑢 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))∀𝑣 ∈
(BaseSet‘if(𝑈 ∈
CHilOLD, 𝑈, ⟨⟨ +
, · ⟩, abs⟩))(𝑢(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑣)) = ((𝑇‘𝑢)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑣)) |
44 | | oveq1 7365 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝑦(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥)) = (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥))) |
45 | 44 | cbvmptv 5219 |
. . . . . 6
⊢ (𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩)) ↦ (𝑦(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥))) = (𝑤 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
↦ (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥))) |
46 | | fveq2 6843 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑇‘𝑥) = (𝑇‘𝑧)) |
47 | 46 | oveq2d 7374 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥)) = (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑧))) |
48 | 47 | mpteq2dv 5208 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑤 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ↦ (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥))) = (𝑤 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
↦ (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑧)))) |
49 | 45, 48 | eqtrid 2785 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ↦ (𝑦(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥))) = (𝑤 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
↦ (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑧)))) |
50 | 49 | cbvmptv 5219 |
. . . 4
⊢ (𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩)) ↦ (𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ↦ (𝑦(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥)))) = (𝑧 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
↦ (𝑤 ∈
(BaseSet‘if(𝑈 ∈
CHilOLD, 𝑈, ⟨⟨
+ , · ⟩, abs⟩)) ↦ (𝑤(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑧)))) |
51 | | fveq2 6843 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((normCV‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩))‘𝑥) = ((normCV‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩))‘𝑧)) |
52 | 51 | breq1d 5116 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((normCV‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩))‘𝑥) ≤ 1 ↔
((normCV‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))‘𝑧) ≤ 1)) |
53 | 52 | cbvrabv 3416 |
. . . . 5
⊢ {𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩)) ∣ ((normCV‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩))‘𝑥) ≤ 1} = {𝑧 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∣ ((normCV‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))‘𝑧) ≤ 1} |
54 | 53 | imaeq2i 6012 |
. . . 4
⊢ ((𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD,
𝑈, ⟨⟨ + ,
· ⟩, abs⟩)) ↦ (𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ↦ (𝑦(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥)))) “ {𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
∣ ((normCV‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))‘𝑥) ≤ 1}) =
((𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩)) ↦ (𝑦 ∈
(BaseSet‘if(𝑈 ∈
CHilOLD, 𝑈, ⟨⟨
+ , · ⟩, abs⟩)) ↦ (𝑦(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑥)))) “ {𝑧 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
∣ ((normCV‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))‘𝑧) ≤
1}) |
55 | 24, 25, 26, 27, 28, 31, 29, 32, 43, 50, 54 | htthlem 29901 |
. . 3
⊢ ((𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩) LnOp if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩)) ∧ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))∀𝑦 ∈ (BaseSet‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , ·
⟩, abs⟩))(𝑥(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))(𝑇‘𝑦)) = ((𝑇‘𝑥)(·𝑖OLD‘if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))𝑦)) → 𝑇 ∈ (if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) BLnOp
if(𝑈 ∈ CHilOLD, 𝑈, ⟨⟨ + , · ⟩,
abs⟩))) |
56 | 23, 55 | dedth 4545 |
. 2
⊢ (𝑈 ∈ CHilOLD
→ ((𝑇 ∈ 𝐿 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) → 𝑇 ∈ 𝐵)) |
57 | 56 | 3impib 1117 |
1
⊢ ((𝑈 ∈ CHilOLD ∧
𝑇 ∈ 𝐿 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) → 𝑇 ∈ 𝐵) |