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 HL P A Q A S A T A P Q P S Q T S T G A F 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 HL P A Q A S A T A P Q P S Q T S T G A K HL
7 6 hllatd K HL P A Q A S A T A P Q P S Q T S T G A K Lat
8 simpl12 K HL P A Q A S A T A P Q P S Q T S T G A P A
9 eqid Base K = Base K
10 9 3 atbase P A P Base K
11 8 10 syl K HL P A Q A S A T A P Q P S Q T S T G A P Base K
12 simpl13 K HL P A Q A S A T A P Q P S Q T S T G A Q A
13 9 3 atbase Q A Q Base K
14 12 13 syl K HL P A Q A S A T A P Q P S Q T S T G A Q Base K
15 simpl21 K HL P A Q A S A T A P Q P S Q T S T G A S A
16 9 3 atbase S A S Base K
17 15 16 syl K HL P A Q A S A T A P Q P S Q T S T G A S Base K
18 simpl22 K HL P A Q A S A T A P Q P S Q T S T G A T A
19 9 3 atbase T A T Base K
20 18 19 syl K HL P A Q A S A T A P Q P S Q T S T G A T Base K
21 9 1 latj4 K Lat P Base K Q Base K S Base K T Base K P ˙ Q ˙ S ˙ T = P ˙ S ˙ Q ˙ T
22 7 11 14 17 20 21 syl122anc K HL P A Q A S A T A P Q P S Q T S T G A P ˙ Q ˙ S ˙ T = P ˙ S ˙ Q ˙ T
23 simpr K HL P A Q A S A T A P Q P S Q T S T G A G A
24 5 23 eqeltrrid K HL P A Q A S A T A P Q P S Q T S T G A P ˙ S ˙ Q ˙ T A
25 simpl31 K HL P A Q A S A T A P Q P S Q T S T G A P S
26 eqid LLines K = LLines K
27 1 3 26 llni2 K HL P A S A P S P ˙ S LLines K
28 6 8 15 25 27 syl31anc K HL P A Q A S A T A P Q P S Q T S T G A P ˙ S LLines K
29 simpl32 K HL P A Q A S A T A P Q P S Q T S T G A Q T
30 1 3 26 llni2 K HL Q A T A Q T Q ˙ T LLines K
31 6 12 18 29 30 syl31anc K HL P A Q A S A T A P Q P S Q T S T G A Q ˙ T LLines K
32 eqid LPlanes K = LPlanes K
33 1 2 3 26 32 2llnmj K HL P ˙ S LLines K Q ˙ T LLines K P ˙ S ˙ Q ˙ T A P ˙ S ˙ Q ˙ T LPlanes K
34 6 28 31 33 syl3anc K HL P A Q A S A T A P Q P S Q T S T G A P ˙ S ˙ Q ˙ T A P ˙ S ˙ Q ˙ T LPlanes K
35 24 34 mpbid K HL P A Q A S A T A P Q P S Q T S T G A P ˙ S ˙ Q ˙ T LPlanes K
36 22 35 eqeltrd K HL P A Q A S A T A P Q P S Q T S T G A P ˙ Q ˙ S ˙ T LPlanes K
37 simpl23 K HL P A Q A S A T A P Q P S Q T S T G A P Q
38 1 3 26 llni2 K HL P A Q A P Q P ˙ Q LLines K
39 6 8 12 37 38 syl31anc K HL P A Q A S A T A P Q P S Q T S T G A P ˙ Q LLines K
40 simpl33 K HL P A Q A S A T A P Q P S Q T S T G A S T
41 1 3 26 llni2 K HL S A T A S T S ˙ T LLines K
42 6 15 18 40 41 syl31anc K HL P A Q A S A T A P Q P S Q T S T G A S ˙ T LLines K
43 1 2 3 26 32 2llnmj K HL P ˙ Q LLines K S ˙ T LLines K P ˙ Q ˙ S ˙ T A P ˙ Q ˙ S ˙ T LPlanes K
44 6 39 42 43 syl3anc K HL P A Q A S A T A P Q P S Q T S T G A P ˙ Q ˙ S ˙ T A P ˙ Q ˙ S ˙ T LPlanes K
45 36 44 mpbird K HL P A Q A S A T A P Q P S Q T S T G A P ˙ Q ˙ S ˙ T A
46 4 45 eqeltrid K HL P A Q A S A T A P Q P S Q T S T G A F A