Step | Hyp | Ref
| Expression |
1 | | unoplin 29855 |
. . 3
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp) |
2 | | elunop 29807 |
. . . 4
⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦))) |
3 | 2 | simplbi 501 |
. . 3
⊢ (𝑇 ∈ UniOp → 𝑇: ℋ–onto→ ℋ) |
4 | | unopnorm 29852 |
. . . 4
⊢ ((𝑇 ∈ UniOp ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) |
5 | 4 | ralrimiva 3096 |
. . 3
⊢ (𝑇 ∈ UniOp →
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) |
6 | 1, 3, 5 | 3jca 1129 |
. 2
⊢ (𝑇 ∈ UniOp → (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥))) |
7 | | eleq1 2820 |
. . 3
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇 ∈ UniOp ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
UniOp)) |
8 | | eleq1 2820 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇 ∈ LinOp ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
LinOp)) |
9 | | foeq1 6588 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇: ℋ–onto→ ℋ ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ)) |
10 | | 2fveq3 6679 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (normℎ‘(𝑇‘𝑥)) = (normℎ‘(𝑇‘𝑦))) |
11 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (normℎ‘𝑥) =
(normℎ‘𝑦)) |
12 | 10, 11 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 →
((normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) ↔
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦))) |
13 | 12 | cbvralvw 3349 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦)) |
14 | | fveq1 6673 |
. . . . . . . . . 10
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇‘𝑦) = (if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) |
15 | 14 | fveqeq2d 6682 |
. . . . . . . . 9
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
16 | 15 | ralbidv 3109 |
. . . . . . . 8
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(∀𝑦 ∈ ℋ
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
17 | 13, 16 | syl5bb 286 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
18 | 8, 9, 17 | 3anbi123d 1437 |
. . . . . 6
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → ((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) ↔ (if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
if((𝑇 ∈ LinOp ∧
𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦)))) |
19 | | eleq1 2820 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ) ∈ LinOp ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
LinOp)) |
20 | | foeq1 6588 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ): ℋ–onto→ ℋ
↔ if((𝑇 ∈ LinOp
∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ)) |
21 | | fveq1 6673 |
. . . . . . . . 9
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ)‘𝑦) =
(if((𝑇 ∈ LinOp ∧
𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) |
22 | 21 | fveqeq2d 6682 |
. . . . . . . 8
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
((normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
23 | 22 | ralbidv 3109 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(∀𝑦 ∈ ℋ
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
24 | 19, 20, 23 | 3anbi123d 1437 |
. . . . . 6
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → ((( I ↾
ℋ) ∈ LinOp ∧ ( I ↾ ℋ): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦)) ↔ (if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
if((𝑇 ∈ LinOp ∧
𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦)))) |
25 | | idlnop 29927 |
. . . . . . 7
⊢ ( I
↾ ℋ) ∈ LinOp |
26 | | f1oi 6655 |
. . . . . . . 8
⊢ ( I
↾ ℋ): ℋ–1-1-onto→ ℋ |
27 | | f1ofo 6625 |
. . . . . . . 8
⊢ (( I
↾ ℋ): ℋ–1-1-onto→ ℋ → ( I ↾ ℋ):
ℋ–onto→
ℋ) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ ( I
↾ ℋ): ℋ–onto→
ℋ |
29 | | fvresi 6945 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (( I
↾ ℋ)‘𝑦) =
𝑦) |
30 | 29 | fveq2d 6678 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ →
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦)) |
31 | 30 | rgen 3063 |
. . . . . . 7
⊢
∀𝑦 ∈
ℋ (normℎ‘(( I ↾ ℋ)‘𝑦)) =
(normℎ‘𝑦) |
32 | 25, 28, 31 | 3pm3.2i 1340 |
. . . . . 6
⊢ (( I
↾ ℋ) ∈ LinOp ∧ ( I ↾ ℋ): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦)) |
33 | 18, 24, 32 | elimhyp 4479 |
. . . . 5
⊢
(if((𝑇 ∈ LinOp
∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
if((𝑇 ∈ LinOp ∧
𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦)) |
34 | 33 | simp1i 1140 |
. . . 4
⊢ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
LinOp |
35 | 33 | simp2i 1141 |
. . . 4
⊢ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ |
36 | 33 | simp3i 1142 |
. . . 4
⊢
∀𝑦 ∈
ℋ (normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦) |
37 | 34, 35, 36 | lnopunii 29947 |
. . 3
⊢ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
UniOp |
38 | 7, 37 | dedth 4472 |
. 2
⊢ ((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) → 𝑇 ∈ UniOp) |
39 | 6, 38 | impbii 212 |
1
⊢ (𝑇 ∈ UniOp ↔ (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥))) |