Step | Hyp | Ref
| Expression |
1 | | eleq1 2825 |
. 2
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (𝑇 ∈ HrmOp ↔ if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈
HrmOp)) |
2 | | eleq1 2825 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (𝑇 ∈ LinOp ↔ if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈
LinOp)) |
3 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
4 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑇‘𝑥) = (𝑇‘𝑦)) |
5 | 3, 4 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ·ih (𝑇‘𝑥)) = (𝑦 ·ih (𝑇‘𝑦))) |
6 | 5 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ ↔ (𝑦 ·ih (𝑇‘𝑦)) ∈ ℝ)) |
7 | 6 | cbvralvw 3358 |
. . . . . . 7
⊢
(∀𝑥 ∈
ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (𝑇‘𝑦)) ∈ ℝ) |
8 | | fveq1 6716 |
. . . . . . . . . 10
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (𝑇‘𝑦) = (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) |
9 | 8 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (𝑦
·ih (𝑇‘𝑦)) = (𝑦 ·ih
(if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦))) |
10 | 9 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → ((𝑦
·ih (𝑇‘𝑦)) ∈ ℝ ↔ (𝑦 ·ih
(if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ)) |
11 | 10 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) →
(∀𝑦 ∈ ℋ
(𝑦
·ih (𝑇‘𝑦)) ∈ ℝ ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ)) |
12 | 7, 11 | syl5bb 286 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) →
(∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ ↔ ∀𝑦 ∈ ℋ (𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ)) |
13 | 2, 12 | anbi12d 634 |
. . . . 5
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → ((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ) ↔ (if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
∀𝑦 ∈ ℋ
(𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ))) |
14 | | eleq1 2825 |
. . . . . 6
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ) ∈ LinOp ↔ if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈
LinOp)) |
15 | | fveq1 6716 |
. . . . . . . . 9
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ)‘𝑦) =
(if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) |
16 | 15 | oveq2d 7229 |
. . . . . . . 8
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → (𝑦
·ih (( I ↾ ℋ)‘𝑦)) = (𝑦 ·ih
(if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦))) |
17 | 16 | eleq1d 2822 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → ((𝑦
·ih (( I ↾ ℋ)‘𝑦)) ∈ ℝ ↔ (𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ)) |
18 | 17 | ralbidv 3118 |
. . . . . 6
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) →
(∀𝑦 ∈ ℋ
(𝑦
·ih (( I ↾ ℋ)‘𝑦)) ∈ ℝ ↔
∀𝑦 ∈ ℋ
(𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ)) |
19 | 14, 18 | anbi12d 634 |
. . . . 5
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥 ·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) → ((( I ↾
ℋ) ∈ LinOp ∧ ∀𝑦 ∈ ℋ (𝑦 ·ih (( I
↾ ℋ)‘𝑦))
∈ ℝ) ↔ (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
∀𝑦 ∈ ℋ
(𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ))) |
20 | | idlnop 30073 |
. . . . . 6
⊢ ( I
↾ ℋ) ∈ LinOp |
21 | | fvresi 6988 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (( I
↾ ℋ)‘𝑦) =
𝑦) |
22 | 21 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → (𝑦
·ih (( I ↾ ℋ)‘𝑦)) = (𝑦 ·ih 𝑦)) |
23 | | hiidrcl 29176 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ → (𝑦
·ih 𝑦) ∈ ℝ) |
24 | 22, 23 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝑦 ∈ ℋ → (𝑦
·ih (( I ↾ ℋ)‘𝑦)) ∈
ℝ) |
25 | 24 | rgen 3071 |
. . . . . 6
⊢
∀𝑦 ∈
ℋ (𝑦
·ih (( I ↾ ℋ)‘𝑦)) ∈
ℝ |
26 | 20, 25 | pm3.2i 474 |
. . . . 5
⊢ (( I
↾ ℋ) ∈ LinOp ∧ ∀𝑦 ∈ ℋ (𝑦 ·ih (( I
↾ ℋ)‘𝑦))
∈ ℝ) |
27 | 13, 19, 26 | elimhyp 4504 |
. . . 4
⊢
(if((𝑇 ∈ LinOp
∧ ∀𝑥 ∈
ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
∀𝑦 ∈ ℋ
(𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ) |
28 | 27 | simpli 487 |
. . 3
⊢ if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈
LinOp |
29 | 27 | simpri 489 |
. . 3
⊢
∀𝑦 ∈
ℋ (𝑦
·ih (if((𝑇 ∈ LinOp ∧ ∀𝑥 ∈ ℋ (𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ))‘𝑦)) ∈
ℝ |
30 | 28, 29 | lnophmi 30099 |
. 2
⊢ if((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ), 𝑇, ( I ↾ ℋ)) ∈
HrmOp |
31 | 1, 30 | dedth 4497 |
1
⊢ ((𝑇 ∈ LinOp ∧
∀𝑥 ∈ ℋ
(𝑥
·ih (𝑇‘𝑥)) ∈ ℝ) → 𝑇 ∈ HrmOp) |