Description: The projective map of a meet. (Contributed by NM, 25-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmapmeet.b | |
|
pmapmeet.m | |
||
pmapmeet.a | |
||
pmapmeet.p | |
||
Assertion | pmapmeet | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmapmeet.b | |
|
2 | pmapmeet.m | |
|
3 | pmapmeet.a | |
|
4 | pmapmeet.p | |
|
5 | eqid | |
|
6 | simp1 | |
|
7 | simp2 | |
|
8 | simp3 | |
|
9 | 5 2 6 7 8 | meetval | |
10 | 9 | fveq2d | |
11 | prssi | |
|
12 | 11 | 3adant1 | |
13 | prnzg | |
|
14 | 13 | 3ad2ant2 | |
15 | 1 5 4 | pmapglb | |
16 | 6 12 14 15 | syl3anc | |
17 | fveq2 | |
|
18 | fveq2 | |
|
19 | 17 18 | iinxprg | |
20 | 19 | 3adant1 | |
21 | 10 16 20 | 3eqtrd | |