Metamath Proof Explorer


Theorem linepmap

Description: A line described with a projective map. (Contributed by NM, 3-Feb-2012)

Ref Expression
Hypotheses isline2.j ˙ = join K
isline2.a A = Atoms K
isline2.n N = Lines K
isline2.m M = pmap K
Assertion linepmap K Lat P A Q A P Q M P ˙ Q N

Proof

Step Hyp Ref Expression
1 isline2.j ˙ = join K
2 isline2.a A = Atoms K
3 isline2.n N = Lines K
4 isline2.m M = pmap K
5 simpl1 K Lat P A Q A P Q K Lat
6 simpl2 K Lat P A Q A P Q P A
7 eqid Base K = Base K
8 7 2 atbase P A P Base K
9 6 8 syl K Lat P A Q A P Q P Base K
10 simpl3 K Lat P A Q A P Q Q A
11 7 2 atbase Q A Q Base K
12 10 11 syl K Lat P A Q A P Q Q Base K
13 7 1 latjcl K Lat P Base K Q Base K P ˙ Q Base K
14 5 9 12 13 syl3anc K Lat P A Q A P Q P ˙ Q Base K
15 eqid K = K
16 7 15 2 4 pmapval K Lat P ˙ Q Base K M P ˙ Q = r A | r K P ˙ Q
17 5 14 16 syl2anc K Lat P A Q A P Q M P ˙ Q = r A | r K P ˙ Q
18 eqid r A | r K P ˙ Q = r A | r K P ˙ Q
19 15 1 2 3 islinei K Lat P A Q A P Q r A | r K P ˙ Q = r A | r K P ˙ Q r A | r K P ˙ Q N
20 18 19 mpanr2 K Lat P A Q A P Q r A | r K P ˙ Q N
21 17 20 eqeltrd K Lat P A Q A P Q M P ˙ Q N