Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. 2
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (๐ โ HrmOp โ if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
HrmOp)) |
2 | | eleq1 2822 |
. . . . . 6
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (๐ โ LinOp โ if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
LinOp)) |
3 | | id 22 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ ๐ฅ = ๐ฆ) |
4 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐โ๐ฅ) = (๐โ๐ฆ)) |
5 | 3, 4 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ฅ ยทih (๐โ๐ฅ)) = (๐ฆ ยทih (๐โ๐ฆ))) |
6 | 5 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐ฅ ยทih (๐โ๐ฅ)) โ โ โ (๐ฆ ยทih (๐โ๐ฆ)) โ โ)) |
7 | 6 | cbvralvw 3224 |
. . . . . . 7
โข
(โ๐ฅ โ
โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (๐โ๐ฆ)) โ โ) |
8 | | fveq1 6845 |
. . . . . . . . . 10
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (๐โ๐ฆ) = (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) |
9 | 8 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (๐ฆ
ยทih (๐โ๐ฆ)) = (๐ฆ ยทih
(if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ))) |
10 | 9 | eleq1d 2819 |
. . . . . . . 8
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ ((๐ฆ
ยทih (๐โ๐ฆ)) โ โ โ (๐ฆ ยทih
(if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ)) |
11 | 10 | ralbidv 3171 |
. . . . . . 7
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
(โ๐ฆ โ โ
(๐ฆ
ยทih (๐โ๐ฆ)) โ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ)) |
12 | 7, 11 | bitrid 283 |
. . . . . 6
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
(โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ โ โ๐ฆ โ โ (๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ)) |
13 | 2, 12 | anbi12d 632 |
. . . . 5
โข (๐ = if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ ((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ) โ (if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ LinOp โง
โ๐ฆ โ โ
(๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ))) |
14 | | eleq1 2822 |
. . . . . 6
โข (( I
โพ โ) = if((๐
โ LinOp โง โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (( I โพ
โ) โ LinOp โ if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
LinOp)) |
15 | | fveq1 6845 |
. . . . . . . . 9
โข (( I
โพ โ) = if((๐
โ LinOp โง โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (( I โพ
โ)โ๐ฆ) =
(if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) |
16 | 15 | oveq2d 7377 |
. . . . . . . 8
โข (( I
โพ โ) = if((๐
โ LinOp โง โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ (๐ฆ
ยทih (( I โพ โ)โ๐ฆ)) = (๐ฆ ยทih
(if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ))) |
17 | 16 | eleq1d 2819 |
. . . . . . 7
โข (( I
โพ โ) = if((๐
โ LinOp โง โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ ((๐ฆ
ยทih (( I โพ โ)โ๐ฆ)) โ โ โ (๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ)) |
18 | 17 | ralbidv 3171 |
. . . . . 6
โข (( I
โพ โ) = if((๐
โ LinOp โง โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
(โ๐ฆ โ โ
(๐ฆ
ยทih (( I โพ โ)โ๐ฆ)) โ โ โ
โ๐ฆ โ โ
(๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ)) |
19 | 14, 18 | anbi12d 632 |
. . . . 5
โข (( I
โพ โ) = if((๐
โ LinOp โง โ๐ฅ โ โ (๐ฅ ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ ((( I โพ
โ) โ LinOp โง โ๐ฆ โ โ (๐ฆ ยทih (( I
โพ โ)โ๐ฆ))
โ โ) โ (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ LinOp โง
โ๐ฆ โ โ
(๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ))) |
20 | | idlnop 30983 |
. . . . . 6
โข ( I
โพ โ) โ LinOp |
21 | | fvresi 7123 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (( I
โพ โ)โ๐ฆ) =
๐ฆ) |
22 | 21 | oveq2d 7377 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐ฆ
ยทih (( I โพ โ)โ๐ฆ)) = (๐ฆ ยทih ๐ฆ)) |
23 | | hiidrcl 30086 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐ฆ
ยทih ๐ฆ) โ โ) |
24 | 22, 23 | eqeltrd 2834 |
. . . . . . 7
โข (๐ฆ โ โ โ (๐ฆ
ยทih (( I โพ โ)โ๐ฆ)) โ
โ) |
25 | 24 | rgen 3063 |
. . . . . 6
โข
โ๐ฆ โ
โ (๐ฆ
ยทih (( I โพ โ)โ๐ฆ)) โ
โ |
26 | 20, 25 | pm3.2i 472 |
. . . . 5
โข (( I
โพ โ) โ LinOp โง โ๐ฆ โ โ (๐ฆ ยทih (( I
โพ โ)โ๐ฆ))
โ โ) |
27 | 13, 19, 26 | elimhyp 4555 |
. . . 4
โข
(if((๐ โ LinOp
โง โ๐ฅ โ
โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ LinOp โง
โ๐ฆ โ โ
(๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ) |
28 | 27 | simpli 485 |
. . 3
โข if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
LinOp |
29 | 27 | simpri 487 |
. . 3
โข
โ๐ฆ โ
โ (๐ฆ
ยทih (if((๐ โ LinOp โง โ๐ฅ โ โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ))โ๐ฆ)) โ
โ |
30 | 28, 29 | lnophmi 31009 |
. 2
โข if((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ), ๐, ( I โพ โ)) โ
HrmOp |
31 | 1, 30 | dedth 4548 |
1
โข ((๐ โ LinOp โง
โ๐ฅ โ โ
(๐ฅ
ยทih (๐โ๐ฅ)) โ โ) โ ๐ โ HrmOp) |