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	$⊢ \underset{˙}{\lor} = join (K)$
	arglem1.m	$⊢ \underset{˙}{\land} = meet (K)$
	arglem1.a	$⊢ A = Atoms (K)$
	arglem1.f	$⊢ F = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)$
	arglem1.g	$⊢ G = (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)$
Assertion	arglem1N	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (S \in A \land T \in A \land P \neq Q) \land (P \neq S \land Q \neq T \land S \neq T)) \land G \in A) \to F \in A$

Proof

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

Metamath Proof Explorer

Theorem arglem1N

Proof