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 )

Metamath Proof Explorer

Theorem arglem1N

Proof