Metamath Proof Explorer


Theorem 4atexlemex2

Description: Lemma for 4atexlem7 . Show that when C =/= S , C satisfies the existence condition of the consequent. (Contributed by NM, 25-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 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
4thatlem0.c 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) )
Assertion 4atexlemex2 ( ( 𝜑𝐶𝑆 ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )

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 4thatlem0.c 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) )
10 1 2 3 4 5 6 7 8 9 4atexlemc ( 𝜑𝐶𝐴 )
11 10 adantr ( ( 𝜑𝐶𝑆 ) → 𝐶𝐴 )
12 1 2 3 4 5 6 7 8 9 4atexlemnclw ( 𝜑 → ¬ 𝐶 𝑊 )
13 12 adantr ( ( 𝜑𝐶𝑆 ) → ¬ 𝐶 𝑊 )
14 1 2 3 4 5 6 7 8 4atexlemntlpq ( 𝜑 → ¬ 𝑇 ( 𝑃 𝑄 ) )
15 id ( 𝐶 = 𝑃𝐶 = 𝑃 )
16 9 15 eqtr3id ( 𝐶 = 𝑃 → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) = 𝑃 )
17 16 adantl ( ( 𝜑𝐶 = 𝑃 ) → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) = 𝑃 )
18 1 4atexlemkl ( 𝜑𝐾 ∈ Lat )
19 1 3 5 4atexlemqtb ( 𝜑 → ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
20 1 3 5 4atexlempsb ( 𝜑 → ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
21 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 2 4 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑄 𝑇 ) )
23 18 19 20 22 syl3anc ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑄 𝑇 ) )
24 1 4atexlemk ( 𝜑𝐾 ∈ HL )
25 1 4atexlemq ( 𝜑𝑄𝐴 )
26 1 4atexlemt ( 𝜑𝑇𝐴 )
27 3 5 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑇𝐴 ) → ( 𝑄 𝑇 ) = ( 𝑇 𝑄 ) )
28 24 25 26 27 syl3anc ( 𝜑 → ( 𝑄 𝑇 ) = ( 𝑇 𝑄 ) )
29 23 28 breqtrd ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑇 𝑄 ) )
30 29 adantr ( ( 𝜑𝐶 = 𝑃 ) → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑇 𝑄 ) )
31 17 30 eqbrtrrd ( ( 𝜑𝐶 = 𝑃 ) → 𝑃 ( 𝑇 𝑄 ) )
32 1 4atexlemkc ( 𝜑𝐾 ∈ CvLat )
33 1 4atexlemp ( 𝜑𝑃𝐴 )
34 1 4atexlempnq ( 𝜑𝑃𝑄 )
35 2 3 5 cvlatexch2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑇𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑃 ( 𝑇 𝑄 ) → 𝑇 ( 𝑃 𝑄 ) ) )
36 32 33 26 25 34 35 syl131anc ( 𝜑 → ( 𝑃 ( 𝑇 𝑄 ) → 𝑇 ( 𝑃 𝑄 ) ) )
37 36 adantr ( ( 𝜑𝐶 = 𝑃 ) → ( 𝑃 ( 𝑇 𝑄 ) → 𝑇 ( 𝑃 𝑄 ) ) )
38 31 37 mpd ( ( 𝜑𝐶 = 𝑃 ) → 𝑇 ( 𝑃 𝑄 ) )
39 38 ex ( 𝜑 → ( 𝐶 = 𝑃𝑇 ( 𝑃 𝑄 ) ) )
40 39 necon3bd ( 𝜑 → ( ¬ 𝑇 ( 𝑃 𝑄 ) → 𝐶𝑃 ) )
41 14 40 mpd ( 𝜑𝐶𝑃 )
42 41 adantr ( ( 𝜑𝐶𝑆 ) → 𝐶𝑃 )
43 simpr ( ( 𝜑𝐶𝑆 ) → 𝐶𝑆 )
44 21 2 4 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑃 𝑆 ) )
45 18 19 20 44 syl3anc ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) ( 𝑃 𝑆 ) )
46 9 45 eqbrtrid ( 𝜑𝐶 ( 𝑃 𝑆 ) )
47 46 adantr ( ( 𝜑𝐶𝑆 ) → 𝐶 ( 𝑃 𝑆 ) )
48 1 4atexlems ( 𝜑𝑆𝐴 )
49 1 2 3 5 4atexlempns ( 𝜑𝑃𝑆 )
50 5 2 3 cvlsupr2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑆𝐴𝐶𝐴 ) ∧ 𝑃𝑆 ) → ( ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) ↔ ( 𝐶𝑃𝐶𝑆𝐶 ( 𝑃 𝑆 ) ) ) )
51 32 33 48 10 49 50 syl131anc ( 𝜑 → ( ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) ↔ ( 𝐶𝑃𝐶𝑆𝐶 ( 𝑃 𝑆 ) ) ) )
52 51 adantr ( ( 𝜑𝐶𝑆 ) → ( ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) ↔ ( 𝐶𝑃𝐶𝑆𝐶 ( 𝑃 𝑆 ) ) ) )
53 42 43 47 52 mpbir3and ( ( 𝜑𝐶𝑆 ) → ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) )
54 breq1 ( 𝑧 = 𝐶 → ( 𝑧 𝑊𝐶 𝑊 ) )
55 54 notbid ( 𝑧 = 𝐶 → ( ¬ 𝑧 𝑊 ↔ ¬ 𝐶 𝑊 ) )
56 oveq2 ( 𝑧 = 𝐶 → ( 𝑃 𝑧 ) = ( 𝑃 𝐶 ) )
57 oveq2 ( 𝑧 = 𝐶 → ( 𝑆 𝑧 ) = ( 𝑆 𝐶 ) )
58 56 57 eqeq12d ( 𝑧 = 𝐶 → ( ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ↔ ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) ) )
59 55 58 anbi12d ( 𝑧 = 𝐶 → ( ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ↔ ( ¬ 𝐶 𝑊 ∧ ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) ) ) )
60 59 rspcev ( ( 𝐶𝐴 ∧ ( ¬ 𝐶 𝑊 ∧ ( 𝑃 𝐶 ) = ( 𝑆 𝐶 ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
61 11 13 53 60 syl12anc ( ( 𝜑𝐶𝑆 ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )