Proof of Theorem phiexg
Step | Hyp | Ref
| Expression |
1 | | dfphi2 4569 |
. 2
Phi ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![A](_ca.gif) ![)](rp.gif) |
2 | | addcexlem 4382 |
. . . . . . 7
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
3 | | 1cex 4142 |
. . . . . . . . 9
1c
![_V](rmcv.gif) |
4 | 3 | pw1ex 4303 |
. . . . . . . 8
1
1c
![_V](rmcv.gif) |
5 | 4 | pw1ex 4303 |
. . . . . . 7
1 1
1c
![_V](rmcv.gif) |
6 | 2, 5 | imakex 4300 |
. . . . . 6
![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
7 | 6 | imagekex 4312 |
. . . . 5
Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
8 | | nncex 4396 |
. . . . . 6
Nn ![_V](rmcv.gif) |
9 | | vvex 4109 |
. . . . . 6
![_V](rmcv.gif) |
10 | 8, 9 | xpkex 4289 |
. . . . 5
Nn k ![_V](rmcv.gif)
![_V](rmcv.gif) |
11 | 7, 10 | inex 4105 |
. . . 4
Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) ![_V](rmcv.gif) |
12 | | idkex 4314 |
. . . . 5
k
![_V](rmcv.gif) |
13 | 8 | complex 4104 |
. . . . . 6
∼ Nn ![_V](rmcv.gif) |
14 | 13, 9 | xpkex 4289 |
. . . . 5
∼ Nn k ![_V](rmcv.gif)
![_V](rmcv.gif) |
15 | 12, 14 | inex 4105 |
. . . 4
k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif)
![_V](rmcv.gif) |
16 | 11, 15 | unex 4106 |
. . 3
![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
17 | | imakexg 4299 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![V](_cv.gif) ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![A](_ca.gif)
![_V](rmcv.gif) ![)](rp.gif) |
18 | 16, 17 | mpan 651 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Imagek![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c Nn k ![_V](rmcv.gif) ![)](rp.gif) k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k![A](_ca.gif)
![_V](rmcv.gif) ![)](rp.gif) |
19 | 1, 18 | syl5eqel 2437 |
1
![(](lp.gif)
Phi ![_V](rmcv.gif) ![)](rp.gif) |