Step | Hyp | Ref
| Expression |
1 | | unoplin 30911 |
. . 3
โข (๐ โ UniOp โ ๐ โ LinOp) |
2 | | elunop 30863 |
. . . 4
โข (๐ โ UniOp โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) |
3 | 2 | simplbi 499 |
. . 3
โข (๐ โ UniOp โ ๐: โโontoโ โ) |
4 | | unopnorm 30908 |
. . . 4
โข ((๐ โ UniOp โง ๐ฅ โ โ) โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)) |
5 | 4 | ralrimiva 3140 |
. . 3
โข (๐ โ UniOp โ
โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)) |
6 | 1, 3, 5 | 3jca 1129 |
. 2
โข (๐ โ UniOp โ (๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ))) |
7 | | eleq1 2822 |
. . 3
โข (๐ = if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (๐ โ UniOp โ if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
UniOp)) |
8 | | eleq1 2822 |
. . . . . . 7
โข (๐ = if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (๐ โ LinOp โ if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
LinOp)) |
9 | | foeq1 6756 |
. . . . . . 7
โข (๐ = if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (๐: โโontoโ โ โ if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)): โโontoโ โ)) |
10 | | 2fveq3 6851 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (normโโ(๐โ๐ฅ)) = (normโโ(๐โ๐ฆ))) |
11 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (normโโ๐ฅ) =
(normโโ๐ฆ)) |
12 | 10, 11 | eqeq12d 2749 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ
((normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) โ
(normโโ(๐โ๐ฆ)) = (normโโ๐ฆ))) |
13 | 12 | cbvralvw 3224 |
. . . . . . . 8
โข
(โ๐ฅ โ
โ (normโโ(๐โ๐ฅ)) = (normโโ๐ฅ) โ โ๐ฆ โ โ
(normโโ(๐โ๐ฆ)) = (normโโ๐ฆ)) |
14 | | fveq1 6845 |
. . . . . . . . . 10
โข (๐ = if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (๐โ๐ฆ) = (if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ))โ๐ฆ)) |
15 | 14 | fveqeq2d 6854 |
. . . . . . . . 9
โข (๐ = if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
((normโโ(๐โ๐ฆ)) = (normโโ๐ฆ) โ
(normโโ(if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ))โ๐ฆ)) =
(normโโ๐ฆ))) |
16 | 15 | ralbidv 3171 |
. . . . . . . 8
โข (๐ = if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
(โ๐ฆ โ โ
(normโโ(๐โ๐ฆ)) = (normโโ๐ฆ) โ โ๐ฆ โ โ
(normโโ(if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ))โ๐ฆ)) =
(normโโ๐ฆ))) |
17 | 13, 16 | bitrid 283 |
. . . . . . 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 2822 |
. . . . . . 7
โข (( I
โพ โ) = if((๐
โ LinOp โง ๐:
โโontoโ โ โง
โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (( I โพ
โ) โ LinOp โ if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
LinOp)) |
20 | | foeq1 6756 |
. . . . . . 7
โข (( I
โพ โ) = if((๐
โ LinOp โง ๐:
โโontoโ โ โง
โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (( I โพ
โ): โโontoโ โ
โ if((๐ โ LinOp
โง ๐:
โโontoโ โ โง
โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)): โโontoโ โ)) |
21 | | fveq1 6845 |
. . . . . . . . 9
โข (( I
โพ โ) = if((๐
โ LinOp โง ๐:
โโontoโ โ โง
โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ (( I โพ
โ)โ๐ฆ) =
(if((๐ โ LinOp โง
๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ))โ๐ฆ)) |
22 | 21 | fveqeq2d 6854 |
. . . . . . . 8
โข (( I
โพ โ) = if((๐
โ LinOp โง ๐:
โโontoโ โ โง
โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
((normโโ(( I โพ โ)โ๐ฆ)) = (normโโ๐ฆ) โ
(normโโ(if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ))โ๐ฆ)) =
(normโโ๐ฆ))) |
23 | 22 | ralbidv 3171 |
. . . . . . 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 30983 |
. . . . . . 7
โข ( I
โพ โ) โ LinOp |
26 | | f1oi 6826 |
. . . . . . . 8
โข ( I
โพ โ): โโ1-1-ontoโ โ |
27 | | f1ofo 6795 |
. . . . . . . 8
โข (( I
โพ โ): โโ1-1-ontoโ โ โ ( I โพ โ):
โโontoโ
โ) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
โข ( I
โพ โ): โโontoโ
โ |
29 | | fvresi 7123 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (( I
โพ โ)โ๐ฆ) =
๐ฆ) |
30 | 29 | fveq2d 6850 |
. . . . . . . 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 4555 |
. . . . 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 31003 |
. . 3
โข if((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)), ๐, ( I โพ โ)) โ
UniOp |
38 | 7, 37 | dedth 4548 |
. 2
โข ((๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ)) โ ๐ โ UniOp) |
39 | 6, 38 | impbii 208 |
1
โข (๐ โ UniOp โ (๐ โ LinOp โง ๐: โโontoโ โ โง โ๐ฅ โ โ
(normโโ(๐โ๐ฅ)) = (normโโ๐ฅ))) |