Metamath Proof Explorer

Theorem dalem8

Description: Lemma for dath . Plane Z belongs to the 3-dimensional space. (Contributed by NM, 21-Jul-2012)

Ref Expression
Hypotheses dalema.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
dalemc.l ⊢ ≤ = ( le ‘ 𝐾 )
dalemc.j ⊢ ∨ = ( join ‘ 𝐾 )
dalemc.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dalem6.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
dalem6.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
dalem6.z ⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
dalem6.w ⊢ 𝑊 = ( 𝑌 ∨ 𝐶 )
Assertion dalem8 ( 𝜑 → 𝑍 ≤ 𝑊 )

Proof

Step Hyp Ref Expression
1 dalema.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
2 dalemc.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dalemc.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dalemc.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dalem6.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
6 dalem6.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
7 dalem6.z ⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
8 dalem6.w ⊢ 𝑊 = ( 𝑌 ∨ 𝐶 )
9 1 2 3 4 5 6 7 8 dalem6 ⊢ ( 𝜑 → 𝑆 ≤ 𝑊 )
10 1 2 3 4 5 6 7 8 dalem7 ⊢ ( 𝜑 → 𝑇 ≤ 𝑊 )
11 1 dalemkelat ⊢ ( 𝜑 → 𝐾 ∈ Lat )
12 1 4 dalemseb ⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
13 1 4 dalemteb ⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
14 1 5 dalemyeb ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
15 1 4 dalemceb ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐾 ) )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑌 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
18 11 14 15 17 syl3anc ⊢ ( 𝜑 → ( 𝑌 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
19 8 18 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
20 16 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ 𝑊 ∧ 𝑇 ≤ 𝑊 ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ) )
21 11 12 13 19 20 syl13anc ⊢ ( 𝜑 → ( ( 𝑆 ≤ 𝑊 ∧ 𝑇 ≤ 𝑊 ) ↔ ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ) )
22 9 10 21 mpbi2and ⊢ ( 𝜑 → ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 )
23 1 2 3 4 5 6 8 dalem5 ⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
24 1 3 4 dalemsjteb ⊢ ( 𝜑 → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
25 1 4 dalemueb ⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
26 16 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ) )
27 11 24 25 19 26 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑆 ∨ 𝑇 ) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 ) )
28 22 23 27 mpbi2and ⊢ ( 𝜑 → ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) ≤ 𝑊 )
29 7 28 eqbrtrid ⊢ ( 𝜑 → 𝑍 ≤ 𝑊 )