This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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