Metamath Proof Explorer


Theorem 4atex

Description: Whenever there are at least 4 atoms under P .\/ Q (specifically, P , Q , r , and ( P .\/ Q ) ./\ W ), there are also at least 4 atoms under P .\/ S . This proves the statement in Lemma E of Crawley p. 114, last line, "...p \/ q/0 and hence p \/ s/0 contains at least four atoms..." Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . (Contributed by NM, 27-May-2013)

Ref Expression
Hypotheses 4that.l = ( le ‘ 𝐾 )
4that.j = ( join ‘ 𝐾 )
4that.a 𝐴 = ( Atoms ‘ 𝐾 )
4that.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion 4atex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 4that.l = ( le ‘ 𝐾 )
2 4that.j = ( join ‘ 𝐾 )
3 4that.a 𝐴 = ( Atoms ‘ 𝐾 )
4 4that.h 𝐻 = ( LHyp ‘ 𝐾 )
5 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑃𝐴 )
6 5 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆 = 𝑃 ) → 𝑃𝐴 )
7 simp21r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ¬ 𝑃 𝑊 )
8 7 ad2antrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆 = 𝑃 ) → ¬ 𝑃 𝑊 )
9 oveq1 ( 𝑃 = 𝑆 → ( 𝑃 𝑃 ) = ( 𝑆 𝑃 ) )
10 9 eqcoms ( 𝑆 = 𝑃 → ( 𝑃 𝑃 ) = ( 𝑆 𝑃 ) )
11 10 adantl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆 = 𝑃 ) → ( 𝑃 𝑃 ) = ( 𝑆 𝑃 ) )
12 breq1 ( 𝑧 = 𝑃 → ( 𝑧 𝑊𝑃 𝑊 ) )
13 12 notbid ( 𝑧 = 𝑃 → ( ¬ 𝑧 𝑊 ↔ ¬ 𝑃 𝑊 ) )
14 oveq2 ( 𝑧 = 𝑃 → ( 𝑃 𝑧 ) = ( 𝑃 𝑃 ) )
15 oveq2 ( 𝑧 = 𝑃 → ( 𝑆 𝑧 ) = ( 𝑆 𝑃 ) )
16 14 15 eqeq12d ( 𝑧 = 𝑃 → ( ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ↔ ( 𝑃 𝑃 ) = ( 𝑆 𝑃 ) ) )
17 13 16 anbi12d ( 𝑧 = 𝑃 → ( ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ↔ ( ¬ 𝑃 𝑊 ∧ ( 𝑃 𝑃 ) = ( 𝑆 𝑃 ) ) ) )
18 17 rspcev ( ( 𝑃𝐴 ∧ ( ¬ 𝑃 𝑊 ∧ ( 𝑃 𝑃 ) = ( 𝑆 𝑃 ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
19 6 8 11 18 syl12anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆 = 𝑃 ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
20 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) )
21 20 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆 = 𝑄 ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) )
22 breq1 ( 𝑟 = 𝑧 → ( 𝑟 𝑊𝑧 𝑊 ) )
23 22 notbid ( 𝑟 = 𝑧 → ( ¬ 𝑟 𝑊 ↔ ¬ 𝑧 𝑊 ) )
24 oveq2 ( 𝑟 = 𝑧 → ( 𝑃 𝑟 ) = ( 𝑃 𝑧 ) )
25 oveq2 ( 𝑟 = 𝑧 → ( 𝑄 𝑟 ) = ( 𝑄 𝑧 ) )
26 24 25 eqeq12d ( 𝑟 = 𝑧 → ( ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ↔ ( 𝑃 𝑧 ) = ( 𝑄 𝑧 ) ) )
27 23 26 anbi12d ( 𝑟 = 𝑧 → ( ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ↔ ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑄 𝑧 ) ) ) )
28 27 cbvrexvw ( ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ↔ ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑄 𝑧 ) ) )
29 oveq1 ( 𝑆 = 𝑄 → ( 𝑆 𝑧 ) = ( 𝑄 𝑧 ) )
30 29 eqeq2d ( 𝑆 = 𝑄 → ( ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ↔ ( 𝑃 𝑧 ) = ( 𝑄 𝑧 ) ) )
31 30 anbi2d ( 𝑆 = 𝑄 → ( ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ↔ ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑄 𝑧 ) ) ) )
32 31 rexbidv ( 𝑆 = 𝑄 → ( ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ↔ ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑄 𝑧 ) ) ) )
33 28 32 bitr4id ( 𝑆 = 𝑄 → ( ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ↔ ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) )
34 33 adantl ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆 = 𝑄 ) → ( ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ↔ ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) )
35 21 34 mpbid ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆 = 𝑄 ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
36 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑄𝐴 )
37 36 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑄𝐴 )
38 simp22r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ¬ 𝑄 𝑊 )
39 38 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → ¬ 𝑄 𝑊 )
40 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑃𝑄 )
41 40 necomd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑄𝑃 )
42 41 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑄𝑃 )
43 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑆𝑄 )
44 43 necomd ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑄𝑆 )
45 simpllr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑆 ( 𝑃 𝑄 ) )
46 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝐾 ∈ HL )
47 hlcvl ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
48 46 47 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝐾 ∈ CvLat )
49 48 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝐾 ∈ CvLat )
50 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → 𝑆𝐴 )
51 50 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑆𝐴 )
52 5 ad3antrrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑃𝐴 )
53 simplr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑆𝑃 )
54 1 2 3 cvlatexch1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑆𝐴𝑄𝐴𝑃𝐴 ) ∧ 𝑆𝑃 ) → ( 𝑆 ( 𝑃 𝑄 ) → 𝑄 ( 𝑃 𝑆 ) ) )
55 49 51 37 52 53 54 syl131anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → ( 𝑆 ( 𝑃 𝑄 ) → 𝑄 ( 𝑃 𝑆 ) ) )
56 45 55 mpd ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑄 ( 𝑃 𝑆 ) )
57 53 necomd ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → 𝑃𝑆 )
58 3 1 2 cvlsupr2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑆𝐴𝑄𝐴 ) ∧ 𝑃𝑆 ) → ( ( 𝑃 𝑄 ) = ( 𝑆 𝑄 ) ↔ ( 𝑄𝑃𝑄𝑆𝑄 ( 𝑃 𝑆 ) ) ) )
59 49 52 51 37 57 58 syl131anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → ( ( 𝑃 𝑄 ) = ( 𝑆 𝑄 ) ↔ ( 𝑄𝑃𝑄𝑆𝑄 ( 𝑃 𝑆 ) ) ) )
60 42 44 56 59 mpbir3and ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → ( 𝑃 𝑄 ) = ( 𝑆 𝑄 ) )
61 breq1 ( 𝑧 = 𝑄 → ( 𝑧 𝑊𝑄 𝑊 ) )
62 61 notbid ( 𝑧 = 𝑄 → ( ¬ 𝑧 𝑊 ↔ ¬ 𝑄 𝑊 ) )
63 oveq2 ( 𝑧 = 𝑄 → ( 𝑃 𝑧 ) = ( 𝑃 𝑄 ) )
64 oveq2 ( 𝑧 = 𝑄 → ( 𝑆 𝑧 ) = ( 𝑆 𝑄 ) )
65 63 64 eqeq12d ( 𝑧 = 𝑄 → ( ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ↔ ( 𝑃 𝑄 ) = ( 𝑆 𝑄 ) ) )
66 62 65 anbi12d ( 𝑧 = 𝑄 → ( ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ↔ ( ¬ 𝑄 𝑊 ∧ ( 𝑃 𝑄 ) = ( 𝑆 𝑄 ) ) ) )
67 66 rspcev ( ( 𝑄𝐴 ∧ ( ¬ 𝑄 𝑊 ∧ ( 𝑃 𝑄 ) = ( 𝑆 𝑄 ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
68 37 39 60 67 syl12anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) ∧ 𝑆𝑄 ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
69 35 68 pm2.61dane ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑆𝑃 ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
70 19 69 pm2.61dane ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ 𝑆 ( 𝑃 𝑄 ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
71 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
72 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) )
73 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑃𝑄 )
74 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
75 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) )
76 1 2 3 4 4atexlem7 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
77 71 72 73 74 75 76 syl113anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
78 70 77 pm2.61dan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )