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 ‘ 𝐾 )
	arglem1.m	⊢ ∧ = ( meet ‘ 𝐾 )
	arglem1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	arglem1.f	⊢ 𝐹 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) )
	arglem1.g	⊢ 𝐺 = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) )
Assertion	arglem1N	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐹 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		arglem1.j	⊢ ∨ = ( join ‘ 𝐾 )
2		arglem1.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		arglem1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		arglem1.f	⊢ 𝐹 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) )
5		arglem1.g	⊢ 𝐺 = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) )
6		simpl11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐾 ∈ HL )
7	6	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐾 ∈ Lat )
8		simpl12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
9		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10	9 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
11	8 10	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
12		simpl13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
13	9 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
14	12 13	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
15		simpl21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑆 ∈ 𝐴 )
16	9 3	atbase	⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
17	15 16	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
18		simpl22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑇 ∈ 𝐴 )
19	9 3	atbase	⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
20	18 19	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
21	9 1	latj4	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) )
22	7 11 14 17 20 21	syl122anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) )
23		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐺 ∈ 𝐴 )
24	5 23	eqeltrrid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ 𝐴 )
25		simpl31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ≠ 𝑆 )
26		eqid	⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
27	1 3 26	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑆 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
28	6 8 15 25 27	syl31anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
29		simpl32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑄 ≠ 𝑇 )
30	1 3 26	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑇 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
31	6 12 18 29 30	syl31anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
32		eqid	⊢ ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 )
33	1 2 3 26 32	2llnmj	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) )
34	6 28 31 33	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) )
35	24 34	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∨ ( 𝑄 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) )
36	22 35	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) )
37		simpl23	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑃 ≠ 𝑄 )
38	1 3 26	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) )
39	6 8 12 37 38	syl31anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) )
40		simpl33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝑆 ≠ 𝑇 )
41	1 3 26	llni2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ 𝑆 ≠ 𝑇 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
42	6 15 18 40 41	syl31anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
43	1 2 3 26 32	2llnmj	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) )
44	6 39 42 43	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑆 ∨ 𝑇 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) )
45	36 44	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 )
46	4 45	eqeltrid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑃 ≠ 𝑆 ∧ 𝑄 ≠ 𝑇 ∧ 𝑆 ≠ 𝑇 ) ) ∧ 𝐺 ∈ 𝐴 ) → 𝐹 ∈ 𝐴 )