This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )