Proof of Theorem proj2eq
Step | Hyp | Ref
| Expression |
1 | | imakeq2 4225 |
. 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)
![(](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![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | 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) |
3 | | 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![B](_cb.gif) ![)](rp.gif) |
4 | 1, 2, 3 | 3eqtr4g 2410 |
1
![(](lp.gif)
Proj2
Proj2 ![B](_cb.gif) ![)](rp.gif) |