Metamath Proof Explorer


Theorem arglem1N

Description: Lemma for Desargues's law. Theorem 13.3 of Crawley p. 110, third and fourth lines from bottom. In these lemmas, P , Q , R , S , T , U , C , D , E , F , and G represent Crawley's a_0, a_1, a_2, b_0, b_1, b_2, c, z_0, z_1, z_2, and p respectively. (Contributed by NM, 28-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses arglem1.j
|- .\/ = ( join ` K )
arglem1.m
|- ./\ = ( meet ` K )
arglem1.a
|- A = ( Atoms ` K )
arglem1.f
|- F = ( ( P .\/ Q ) ./\ ( S .\/ T ) )
arglem1.g
|- G = ( ( P .\/ S ) ./\ ( Q .\/ T ) )
Assertion arglem1N
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> F e. A )

Proof

Step Hyp Ref Expression
1 arglem1.j
 |-  .\/ = ( join ` K )
2 arglem1.m
 |-  ./\ = ( meet ` K )
3 arglem1.a
 |-  A = ( Atoms ` K )
4 arglem1.f
 |-  F = ( ( P .\/ Q ) ./\ ( S .\/ T ) )
5 arglem1.g
 |-  G = ( ( P .\/ S ) ./\ ( Q .\/ T ) )
6 simpl11
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> K e. HL )
7 6 hllatd
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> K e. Lat )
8 simpl12
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> P e. A )
9 eqid
 |-  ( Base ` K ) = ( Base ` K )
10 9 3 atbase
 |-  ( P e. A -> P e. ( Base ` K ) )
11 8 10 syl
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> P e. ( Base ` K ) )
12 simpl13
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> Q e. A )
13 9 3 atbase
 |-  ( Q e. A -> Q e. ( Base ` K ) )
14 12 13 syl
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> Q e. ( Base ` K ) )
15 simpl21
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> S e. A )
16 9 3 atbase
 |-  ( S e. A -> S e. ( Base ` K ) )
17 15 16 syl
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> S e. ( Base ` K ) )
18 simpl22
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> T e. A )
19 9 3 atbase
 |-  ( T e. A -> T e. ( Base ` K ) )
20 18 19 syl
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> T e. ( Base ` K ) )
21 9 1 latj4
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) ) ) -> ( ( P .\/ Q ) .\/ ( S .\/ T ) ) = ( ( P .\/ S ) .\/ ( Q .\/ T ) ) )
22 7 11 14 17 20 21 syl122anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( P .\/ Q ) .\/ ( S .\/ T ) ) = ( ( P .\/ S ) .\/ ( Q .\/ T ) ) )
23 simpr
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> G e. A )
24 5 23 eqeltrrid
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( P .\/ S ) ./\ ( Q .\/ T ) ) e. A )
25 simpl31
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> P =/= S )
26 eqid
 |-  ( LLines ` K ) = ( LLines ` K )
27 1 3 26 llni2
 |-  ( ( ( K e. HL /\ P e. A /\ S e. A ) /\ P =/= S ) -> ( P .\/ S ) e. ( LLines ` K ) )
28 6 8 15 25 27 syl31anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( P .\/ S ) e. ( LLines ` K ) )
29 simpl32
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> Q =/= T )
30 1 3 26 llni2
 |-  ( ( ( K e. HL /\ Q e. A /\ T e. A ) /\ Q =/= T ) -> ( Q .\/ T ) e. ( LLines ` K ) )
31 6 12 18 29 30 syl31anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( Q .\/ T ) e. ( LLines ` K ) )
32 eqid
 |-  ( LPlanes ` K ) = ( LPlanes ` K )
33 1 2 3 26 32 2llnmj
 |-  ( ( K e. HL /\ ( P .\/ S ) e. ( LLines ` K ) /\ ( Q .\/ T ) e. ( LLines ` K ) ) -> ( ( ( P .\/ S ) ./\ ( Q .\/ T ) ) e. A <-> ( ( P .\/ S ) .\/ ( Q .\/ T ) ) e. ( LPlanes ` K ) ) )
34 6 28 31 33 syl3anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( ( P .\/ S ) ./\ ( Q .\/ T ) ) e. A <-> ( ( P .\/ S ) .\/ ( Q .\/ T ) ) e. ( LPlanes ` K ) ) )
35 24 34 mpbid
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( P .\/ S ) .\/ ( Q .\/ T ) ) e. ( LPlanes ` K ) )
36 22 35 eqeltrd
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( P .\/ Q ) .\/ ( S .\/ T ) ) e. ( LPlanes ` K ) )
37 simpl23
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> P =/= Q )
38 1 3 26 llni2
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( LLines ` K ) )
39 6 8 12 37 38 syl31anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( P .\/ Q ) e. ( LLines ` K ) )
40 simpl33
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> S =/= T )
41 1 3 26 llni2
 |-  ( ( ( K e. HL /\ S e. A /\ T e. A ) /\ S =/= T ) -> ( S .\/ T ) e. ( LLines ` K ) )
42 6 15 18 40 41 syl31anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( S .\/ T ) e. ( LLines ` K ) )
43 1 2 3 26 32 2llnmj
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. ( LLines ` K ) /\ ( S .\/ T ) e. ( LLines ` K ) ) -> ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. A <-> ( ( P .\/ Q ) .\/ ( S .\/ T ) ) e. ( LPlanes ` K ) ) )
44 6 39 42 43 syl3anc
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. A <-> ( ( P .\/ Q ) .\/ ( S .\/ T ) ) e. ( LPlanes ` K ) ) )
45 36 44 mpbird
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> ( ( P .\/ Q ) ./\ ( S .\/ T ) ) e. A )
46 4 45 eqeltrid
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> F e. A )