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 ‘ 𝐾 )
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 ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑃𝑄 ) ∧ ( 𝑃𝑆𝑄𝑇𝑆𝑇 ) ) ∧ 𝐺𝐴 ) → 𝐹𝐴 )