Step | Hyp | Ref
| Expression |
1 | | ishst 31198 |
. . . 4
โข (๐ โ CHStates โ (๐:
Cโ โถ โ โง
(normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |
2 | 1 | simp3bi 1148 |
. . 3
โข (๐ โ CHStates โ
โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) |
3 | 2 | ad2antrr 725 |
. 2
โข (((๐ โ CHStates โง ๐ด โ
Cโ ) โง (๐ต โ Cโ
โง ๐ด โ
(โฅโ๐ต))) โ
โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) |
4 | | sseq1 3974 |
. . . . . . 7
โข (๐ฅ = ๐ด โ (๐ฅ โ (โฅโ๐ฆ) โ ๐ด โ (โฅโ๐ฆ))) |
5 | | fveq2 6847 |
. . . . . . . . . 10
โข (๐ฅ = ๐ด โ (๐โ๐ฅ) = (๐โ๐ด)) |
6 | 5 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih (๐โ๐ฆ))) |
7 | 6 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โ ((๐โ๐ด) ยทih (๐โ๐ฆ)) = 0)) |
8 | | fvoveq1 7385 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ (๐โ(๐ฅ โจโ ๐ฆ)) = (๐โ(๐ด โจโ ๐ฆ))) |
9 | 5 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ฅ = ๐ด โ ((๐โ๐ฅ) +โ (๐โ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ))) |
10 | 8, 9 | eqeq12d 2753 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ ((๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐โ(๐ด โจโ ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ)))) |
11 | 7, 10 | anbi12d 632 |
. . . . . . 7
โข (๐ฅ = ๐ด โ ((((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) โ (((๐โ๐ด) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ด โจโ ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ))))) |
12 | 4, 11 | imbi12d 345 |
. . . . . 6
โข (๐ฅ = ๐ด โ ((๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (๐ด โ (โฅโ๐ฆ) โ (((๐โ๐ด) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ด โจโ ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ)))))) |
13 | | fveq2 6847 |
. . . . . . . 8
โข (๐ฆ = ๐ต โ (โฅโ๐ฆ) = (โฅโ๐ต)) |
14 | 13 | sseq2d 3981 |
. . . . . . 7
โข (๐ฆ = ๐ต โ (๐ด โ (โฅโ๐ฆ) โ ๐ด โ (โฅโ๐ต))) |
15 | | fveq2 6847 |
. . . . . . . . . 10
โข (๐ฆ = ๐ต โ (๐โ๐ฆ) = (๐โ๐ต)) |
16 | 15 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ฆ = ๐ต โ ((๐โ๐ด) ยทih (๐โ๐ฆ)) = ((๐โ๐ด) ยทih (๐โ๐ต))) |
17 | 16 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ฆ = ๐ต โ (((๐โ๐ด) ยทih (๐โ๐ฆ)) = 0 โ ((๐โ๐ด) ยทih (๐โ๐ต)) = 0)) |
18 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ฆ = ๐ต โ (๐ด โจโ ๐ฆ) = (๐ด โจโ ๐ต)) |
19 | 18 | fveq2d 6851 |
. . . . . . . . 9
โข (๐ฆ = ๐ต โ (๐โ(๐ด โจโ ๐ฆ)) = (๐โ(๐ด โจโ ๐ต))) |
20 | 15 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ฆ = ๐ต โ ((๐โ๐ด) +โ (๐โ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ต))) |
21 | 19, 20 | eqeq12d 2753 |
. . . . . . . 8
โข (๐ฆ = ๐ต โ ((๐โ(๐ด โจโ ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ)) โ (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)))) |
22 | 17, 21 | anbi12d 632 |
. . . . . . 7
โข (๐ฆ = ๐ต โ ((((๐โ๐ด) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ด โจโ ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ))) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต))))) |
23 | 14, 22 | imbi12d 345 |
. . . . . 6
โข (๐ฆ = ๐ต โ ((๐ด โ (โฅโ๐ฆ) โ (((๐โ๐ด) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ด โจโ ๐ฆ)) = ((๐โ๐ด) +โ (๐โ๐ฆ)))) โ (๐ด โ (โฅโ๐ต) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)))))) |
24 | 12, 23 | rspc2v 3593 |
. . . . 5
โข ((๐ด โ
Cโ โง ๐ต โ Cโ )
โ (โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (๐ด โ (โฅโ๐ต) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)))))) |
25 | 24 | com23 86 |
. . . 4
โข ((๐ด โ
Cโ โง ๐ต โ Cโ )
โ (๐ด โ
(โฅโ๐ต) โ
(โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)))))) |
26 | 25 | impr 456 |
. . 3
โข ((๐ด โ
Cโ โง (๐ต โ Cโ
โง ๐ด โ
(โฅโ๐ต))) โ
(โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต))))) |
27 | 26 | adantll 713 |
. 2
โข (((๐ โ CHStates โง ๐ด โ
Cโ ) โง (๐ต โ Cโ
โง ๐ด โ
(โฅโ๐ต))) โ
(โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต))))) |
28 | 3, 27 | mpd 15 |
1
โข (((๐ โ CHStates โง ๐ด โ
Cโ ) โง (๐ต โ Cโ
โง ๐ด โ
(โฅโ๐ต))) โ
(((๐โ๐ด)
ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)))) |