Proof of Theorem proj2exg
Step | Hyp | Ref
| Expression |
1 | | dfproj22 4577 |
. 2
Proj2 ![(](lp.gif) k ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k![A](_ca.gif) ![)](rp.gif) |
2 | | ssetkex 4294 |
. . . . . . . 8
Sk ![_V](rmcv.gif) |
3 | 2 | ins2kex 4307 |
. . . . . . 7
Ins2k Sk ![_V](rmcv.gif) |
4 | | addcexlem 4382 |
. . . . . . . . . . . . . . . 16
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) |
5 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . 18
1c
![_V](rmcv.gif) |
6 | 5 | pw1ex 4303 |
. . . . . . . . . . . . . . . . 17
1
1c
![_V](rmcv.gif) |
7 | 6 | pw1ex 4303 |
. . . . . . . . . . . . . . . 16
1 1
1c
![_V](rmcv.gif) |
8 | 4, 7 | imakex 4300 |
. . . . . . . . . . . . . . 15
![(](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) |
9 | 8 | imagekex 4312 |
. . . . . . . . . . . . . 14
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) |
10 | | nncex 4396 |
. . . . . . . . . . . . . . 15
Nn ![_V](rmcv.gif) |
11 | | vvex 4109 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
12 | 10, 11 | xpkex 4289 |
. . . . . . . . . . . . . 14
Nn k ![_V](rmcv.gif)
![_V](rmcv.gif) |
13 | 9, 12 | inex 4105 |
. . . . . . . . . . . . 13
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) |
14 | | idkex 4314 |
. . . . . . . . . . . . . 14
k
![_V](rmcv.gif) |
15 | 10 | complex 4104 |
. . . . . . . . . . . . . . 15
∼ Nn ![_V](rmcv.gif) |
16 | 15, 11 | xpkex 4289 |
. . . . . . . . . . . . . 14
∼ Nn k ![_V](rmcv.gif)
![_V](rmcv.gif) |
17 | 14, 16 | inex 4105 |
. . . . . . . . . . . . 13
k ∼ Nn k ![_V](rmcv.gif) ![)](rp.gif)
![_V](rmcv.gif) |
18 | 13, 17 | unex 4106 |
. . . . . . . . . . . 12
![(](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) |
19 | 18 | imagekex 4312 |
. . . . . . . . . . 11
Imagek![(](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) |
20 | 19 | cnvkex 4287 |
. . . . . . . . . 10
kImagek![(](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) |
21 | 20, 2 | cokex 4310 |
. . . . . . . . 9
![(](lp.gif) kImagek![(](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) k Sk
![_V](rmcv.gif) |
22 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) 0c![}](rbrace.gif)
![_V](rmcv.gif) |
23 | 22, 11 | xpkex 4289 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif)
![_V](rmcv.gif) |
24 | 21, 23 | unex 4106 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![_V](rmcv.gif) |
25 | 24 | ins3kex 4308 |
. . . . . . 7
Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![_V](rmcv.gif) |
26 | 3, 25 | symdifex 4108 |
. . . . . 6
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
27 | 26, 7 | imakex 4300 |
. . . . 5
![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c ![_V](rmcv.gif) |
28 | 27 | complex 4104 |
. . . 4
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c ![_V](rmcv.gif) |
29 | 28 | cnvkex 4287 |
. . 3
k
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c ![_V](rmcv.gif) |
30 | | imakexg 4299 |
. . 3
![(](lp.gif) ![(](lp.gif) k ∼ ![(](lp.gif)
Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c ![V](_cv.gif) ![(](lp.gif) k
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k![A](_ca.gif)
![_V](rmcv.gif) ![)](rp.gif) |
31 | 29, 30 | mpan 651 |
. 2
![(](lp.gif) ![(](lp.gif) k ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) ![(](lp.gif) kImagek![(](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) k Sk ![(](lp.gif) ![{](lbrace.gif) 0c![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) k![A](_ca.gif)
![_V](rmcv.gif) ![)](rp.gif) |
32 | 1, 31 | syl5eqel 2437 |
1
![(](lp.gif)
Proj2 ![_V](rmcv.gif) ![)](rp.gif) |