Description: Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pjclem1.1 | |
|
pjclem1.2 | |
||
Assertion | pjclem4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjclem1.1 | |
|
2 | pjclem1.2 | |
|
3 | 1 2 | pjcocli | |
4 | 3 | adantl | |
5 | 2 1 | pjcocli | |
6 | fveq1 | |
|
7 | 6 | eleq1d | |
8 | 5 7 | syl5ibr | |
9 | 8 | imp | |
10 | 4 9 | elind | |
11 | 1 2 | pjcohcli | |
12 | hvsubcl | |
|
13 | 11 12 | mpdan | |
14 | 13 | adantl | |
15 | simpl | |
|
16 | 11 | adantr | |
17 | 1 2 | chincli | |
18 | 17 | cheli | |
19 | 18 | adantl | |
20 | 15 16 19 | 3jca | |
21 | 20 | adantl | |
22 | his2sub | |
|
23 | 21 22 | syl | |
24 | 6 | oveq1d | |
25 | 2 1 | pjadjcoi | |
26 | 18 25 | sylan2 | |
27 | 1 2 | pjclem4a | |
28 | 27 | oveq2d | |
29 | 28 | adantl | |
30 | 26 29 | eqtrd | |
31 | 24 30 | sylan9eq | |
32 | 31 | oveq1d | |
33 | 11 18 | anim12i | |
34 | 33 | adantl | |
35 | hicl | |
|
36 | 34 35 | syl | |
37 | 36 | subidd | |
38 | 23 32 37 | 3eqtr2d | |
39 | 38 | expr | |
40 | 39 | ralrimiv | |
41 | 17 | chshii | |
42 | shocel | |
|
43 | 41 42 | ax-mp | |
44 | 14 40 43 | sylanbrc | |
45 | 17 | pjvi | |
46 | 10 44 45 | syl2anc | |
47 | id | |
|
48 | hvaddsub12 | |
|
49 | 11 47 11 48 | syl3anc | |
50 | hvsubid | |
|
51 | 11 50 | syl | |
52 | 51 | oveq2d | |
53 | ax-hvaddid | |
|
54 | 49 52 53 | 3eqtrd | |
55 | 54 | fveq2d | |
56 | 55 | adantl | |
57 | 46 56 | eqtr3d | |
58 | 57 | ralrimiva | |
59 | 1 | pjfi | |
60 | 2 | pjfi | |
61 | 59 60 | hocofi | |
62 | 17 | pjfi | |
63 | 61 62 | hoeqi | |
64 | 58 63 | sylib | |