Metamath Proof Explorer


Theorem dalem10

Description: Lemma for dath . Atom D belongs to the axis of perspectivity X . (Contributed by NM, 19-Jul-2012)

Ref Expression
Hypotheses dalema.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( 𝑌𝑂𝑍𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) )
dalemc.l = ( le ‘ 𝐾 )
dalemc.j = ( join ‘ 𝐾 )
dalemc.a 𝐴 = ( Atoms ‘ 𝐾 )
dalem10.m = ( meet ‘ 𝐾 )
dalem10.o 𝑂 = ( LPlanes ‘ 𝐾 )
dalem10.y 𝑌 = ( ( 𝑃 𝑄 ) 𝑅 )
dalem10.z 𝑍 = ( ( 𝑆 𝑇 ) 𝑈 )
dalem10.x 𝑋 = ( 𝑌 𝑍 )
dalem10.d 𝐷 = ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) )
Assertion dalem10 ( 𝜑𝐷 𝑋 )

Proof

Step Hyp Ref Expression
1 dalema.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( 𝑌𝑂𝑍𝑂 ) ∧ ( ( ¬ 𝐶 ( 𝑃 𝑄 ) ∧ ¬ 𝐶 ( 𝑄 𝑅 ) ∧ ¬ 𝐶 ( 𝑅 𝑃 ) ) ∧ ( ¬ 𝐶 ( 𝑆 𝑇 ) ∧ ¬ 𝐶 ( 𝑇 𝑈 ) ∧ ¬ 𝐶 ( 𝑈 𝑆 ) ) ∧ ( 𝐶 ( 𝑃 𝑆 ) ∧ 𝐶 ( 𝑄 𝑇 ) ∧ 𝐶 ( 𝑅 𝑈 ) ) ) ) )
2 dalemc.l = ( le ‘ 𝐾 )
3 dalemc.j = ( join ‘ 𝐾 )
4 dalemc.a 𝐴 = ( Atoms ‘ 𝐾 )
5 dalem10.m = ( meet ‘ 𝐾 )
6 dalem10.o 𝑂 = ( LPlanes ‘ 𝐾 )
7 dalem10.y 𝑌 = ( ( 𝑃 𝑄 ) 𝑅 )
8 dalem10.z 𝑍 = ( ( 𝑆 𝑇 ) 𝑈 )
9 dalem10.x 𝑋 = ( 𝑌 𝑍 )
10 dalem10.d 𝐷 = ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) )
11 1 dalemkelat ( 𝜑𝐾 ∈ Lat )
12 1 3 4 dalempjqeb ( 𝜑 → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
13 1 4 dalemreb ( 𝜑𝑅 ∈ ( Base ‘ 𝐾 ) )
14 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15 14 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑄 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
16 11 12 13 15 syl3anc ( 𝜑 → ( 𝑃 𝑄 ) ( ( 𝑃 𝑄 ) 𝑅 ) )
17 1 3 4 dalemsjteb ( 𝜑 → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
18 1 4 dalemueb ( 𝜑𝑈 ∈ ( Base ‘ 𝐾 ) )
19 14 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 𝑇 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
20 11 17 18 19 syl3anc ( 𝜑 → ( 𝑆 𝑇 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
21 1 6 dalemyeb ( 𝜑𝑌 ∈ ( Base ‘ 𝐾 ) )
22 7 21 eqeltrrid ( 𝜑 → ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
23 1 dalemzeo ( 𝜑𝑍𝑂 )
24 14 6 lplnbase ( 𝑍𝑂𝑍 ∈ ( Base ‘ 𝐾 ) )
25 23 24 syl ( 𝜑𝑍 ∈ ( Base ‘ 𝐾 ) )
26 8 25 eqeltrrid ( 𝜑 → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
27 14 2 5 latmlem12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 𝑄 ) ( ( 𝑃 𝑄 ) 𝑅 ) ∧ ( 𝑆 𝑇 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
28 11 12 22 17 26 27 syl122anc ( 𝜑 → ( ( ( 𝑃 𝑄 ) ( ( 𝑃 𝑄 ) 𝑅 ) ∧ ( 𝑆 𝑇 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ) )
29 16 20 28 mp2and ( 𝜑 → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
30 7 8 oveq12i ( 𝑌 𝑍 ) = ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
31 9 30 eqtri 𝑋 = ( ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
32 29 10 31 3brtr4g ( 𝜑𝐷 𝑋 )