Metamath Proof Explorer


Theorem 4atexlemntlpq

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) )
4thatlem0.l = ( le ‘ 𝐾 )
4thatlem0.j = ( join ‘ 𝐾 )
4thatlem0.m = ( meet ‘ 𝐾 )
4thatlem0.a 𝐴 = ( Atoms ‘ 𝐾 )
4thatlem0.h 𝐻 = ( LHyp ‘ 𝐾 )
4thatlem0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
4thatlem0.v 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
Assertion 4atexlemntlpq ( 𝜑 → ¬ 𝑇 ( 𝑃 𝑄 ) )

Proof

Step Hyp Ref Expression
1 4thatlem.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) )
2 4thatlem0.l = ( le ‘ 𝐾 )
3 4thatlem0.j = ( join ‘ 𝐾 )
4 4thatlem0.m = ( meet ‘ 𝐾 )
5 4thatlem0.a 𝐴 = ( Atoms ‘ 𝐾 )
6 4thatlem0.h 𝐻 = ( LHyp ‘ 𝐾 )
7 4thatlem0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 4thatlem0.v 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
9 1 2 3 4 5 6 7 8 4atexlemtlw ( 𝜑𝑇 𝑊 )
10 1 4atexlemkc ( 𝜑𝐾 ∈ CvLat )
11 1 2 3 4 5 6 7 4atexlemu ( 𝜑𝑈𝐴 )
12 1 2 3 4 5 6 7 8 4atexlemv ( 𝜑𝑉𝐴 )
13 1 4atexlemt ( 𝜑𝑇𝐴 )
14 1 2 3 4 5 6 7 8 4atexlemunv ( 𝜑𝑈𝑉 )
15 1 4atexlemutvt ( 𝜑 → ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) )
16 5 3 cvlsupr5 ( ( 𝐾 ∈ CvLat ∧ ( 𝑈𝐴𝑉𝐴𝑇𝐴 ) ∧ ( 𝑈𝑉 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) → 𝑇𝑈 )
17 10 11 12 13 14 15 16 syl132anc ( 𝜑𝑇𝑈 )
18 17 adantr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → 𝑇𝑈 )
19 1 4atexlemk ( 𝜑𝐾 ∈ HL )
20 1 4atexlemw ( 𝜑𝑊𝐻 )
21 19 20 jca ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
22 21 adantr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
23 1 4atexlempw ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
24 23 adantr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
25 1 4atexlemq ( 𝜑𝑄𝐴 )
26 25 adantr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → 𝑄𝐴 )
27 13 adantr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → 𝑇𝐴 )
28 1 4atexlempnq ( 𝜑𝑃𝑄 )
29 28 adantr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → 𝑃𝑄 )
30 simpr ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → 𝑇 ( 𝑃 𝑄 ) )
31 2 3 4 5 6 7 lhpat3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝑄𝐴𝑇𝐴 ) ∧ ( 𝑃𝑄𝑇 ( 𝑃 𝑄 ) ) ) → ( ¬ 𝑇 𝑊𝑇𝑈 ) )
32 22 24 26 27 29 30 31 syl222anc ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → ( ¬ 𝑇 𝑊𝑇𝑈 ) )
33 18 32 mpbird ( ( 𝜑𝑇 ( 𝑃 𝑄 ) ) → ¬ 𝑇 𝑊 )
34 33 ex ( 𝜑 → ( 𝑇 ( 𝑃 𝑄 ) → ¬ 𝑇 𝑊 ) )
35 9 34 mt2d ( 𝜑 → ¬ 𝑇 ( 𝑃 𝑄 ) )