Step | Hyp | Ref
| Expression |
1 | | unoplin 28779 |
. . 3
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp) |
2 | | elunop 28731 |
. . . 4
⊢ (𝑇 ∈ UniOp ↔ (𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇‘𝑥) ·ih (𝑇‘𝑦)) = (𝑥 ·ih 𝑦))) |
3 | 2 | simplbi 476 |
. . 3
⊢ (𝑇 ∈ UniOp → 𝑇: ℋ–onto→ ℋ) |
4 | | unopnorm 28776 |
. . . 4
⊢ ((𝑇 ∈ UniOp ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) |
5 | 4 | ralrimiva 2966 |
. . 3
⊢ (𝑇 ∈ UniOp →
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) |
6 | 1, 3, 5 | 3jca 1242 |
. 2
⊢ (𝑇 ∈ UniOp → (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥))) |
7 | | eleq1 2689 |
. . 3
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇 ∈ UniOp ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
UniOp)) |
8 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇 ∈ LinOp ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
LinOp)) |
9 | | foeq1 6111 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇: ℋ–onto→ ℋ ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ)) |
10 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑇‘𝑥) = (𝑇‘𝑦)) |
11 | 10 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (normℎ‘(𝑇‘𝑥)) = (normℎ‘(𝑇‘𝑦))) |
12 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (normℎ‘𝑥) =
(normℎ‘𝑦)) |
13 | 11, 12 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 →
((normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) ↔
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦))) |
14 | 13 | cbvralv 3171 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℋ (normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦)) |
15 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (𝑇‘𝑦) = (if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) |
16 | 15 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(normℎ‘(𝑇‘𝑦)) =
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦))) |
17 | 16 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
18 | 17 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(∀𝑦 ∈ ℋ
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
19 | 14, 18 | syl5bb 272 |
. . . . . . 7
⊢ (𝑇 = if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
20 | 8, 9, 19 | 3anbi123d 1399 |
. . . . . 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ℎ‘𝑦)))) |
21 | | eleq1 2689 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ) ∈ LinOp ↔ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
LinOp)) |
22 | | foeq1 6111 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ): ℋ–onto→ ℋ
↔ if((𝑇 ∈ LinOp
∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ)) |
23 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) → (( I ↾
ℋ)‘𝑦) =
(if((𝑇 ∈ LinOp ∧
𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) |
24 | 23 | fveq2d 6195 |
. . . . . . . . 9
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(normℎ‘(( I ↾ ℋ)‘𝑦)) =
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦))) |
25 | 24 | eqeq1d 2624 |
. . . . . . . 8
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
((normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
26 | 25 | ralbidv 2986 |
. . . . . . 7
⊢ (( I
↾ ℋ) = if((𝑇
∈ LinOp ∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) →
(∀𝑦 ∈ ℋ
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦) ↔ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦))) |
27 | 21, 22, 26 | 3anbi123d 1399 |
. . . . . 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ℎ‘𝑦)))) |
28 | | idlnop 28851 |
. . . . . . 7
⊢ ( I
↾ ℋ) ∈ LinOp |
29 | | f1oi 6174 |
. . . . . . . 8
⊢ ( I
↾ ℋ): ℋ–1-1-onto→ ℋ |
30 | | f1ofo 6144 |
. . . . . . . 8
⊢ (( I
↾ ℋ): ℋ–1-1-onto→ ℋ → ( I ↾ ℋ):
ℋ–onto→
ℋ) |
31 | 29, 30 | ax-mp 5 |
. . . . . . 7
⊢ ( I
↾ ℋ): ℋ–onto→
ℋ |
32 | | fvresi 6439 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℋ → (( I
↾ ℋ)‘𝑦) =
𝑦) |
33 | 32 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑦 ∈ ℋ →
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦)) |
34 | 33 | rgen 2922 |
. . . . . . 7
⊢
∀𝑦 ∈
ℋ (normℎ‘(( I ↾ ℋ)‘𝑦)) =
(normℎ‘𝑦) |
35 | 28, 31, 34 | 3pm3.2i 1239 |
. . . . . 6
⊢ (( I
↾ ℋ) ∈ LinOp ∧ ( I ↾ ℋ): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(( I ↾ ℋ)‘𝑦)) = (normℎ‘𝑦)) |
36 | 20, 27, 35 | elimhyp 4146 |
. . . . 5
⊢
(if((𝑇 ∈ LinOp
∧ 𝑇:
ℋ–onto→ ℋ ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈ LinOp ∧
if((𝑇 ∈ LinOp ∧
𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ ∧ ∀𝑦 ∈ ℋ
(normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦)) |
37 | 36 | simp1i 1070 |
. . . 4
⊢ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
LinOp |
38 | 36 | simp2i 1071 |
. . . 4
⊢ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)): ℋ–onto→ ℋ |
39 | 36 | simp3i 1072 |
. . . 4
⊢
∀𝑦 ∈
ℋ (normℎ‘(if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ))‘𝑦)) =
(normℎ‘𝑦) |
40 | 37, 38, 39 | lnopunii 28871 |
. . 3
⊢ if((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)), 𝑇, ( I ↾ ℋ)) ∈
UniOp |
41 | 7, 40 | dedth 4139 |
. 2
⊢ ((𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥)) → 𝑇 ∈ UniOp) |
42 | 6, 41 | impbii 199 |
1
⊢ (𝑇 ∈ UniOp ↔ (𝑇 ∈ LinOp ∧ 𝑇: ℋ–onto→ ℋ ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) = (normℎ‘𝑥))) |