Metamath Proof Explorer


Theorem 4atexlem7

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 ) . With a longer proof, the condition -. S .<_ ( P .\/ Q ) could be eliminated (see 4atex ), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 4that.l = ( le ‘ 𝐾 )
2 4that.j = ( join ‘ 𝐾 )
3 4that.a 𝐴 = ( Atoms ‘ 𝐾 )
4 4that.h 𝐻 = ( LHyp ‘ 𝐾 )
5 simp11l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 simp1r1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
7 6 3ad2ant1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
8 simp1r2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
9 8 3ad2ant1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
10 simp2 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → 𝑟𝐴 )
11 simp3l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ¬ 𝑟 𝑊 )
12 10 11 jca ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ( 𝑟𝐴 ∧ ¬ 𝑟 𝑊 ) )
13 simp1r3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑆𝐴 )
14 13 3ad2ant1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → 𝑆𝐴 )
15 simp3r ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) )
16 simp12 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → 𝑃𝑄 )
17 simp13 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
18 eqid ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
19 1 2 18 3 4 4atexlemex6 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑟𝐴 ∧ ¬ 𝑟 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
20 5 7 9 12 14 15 16 17 19 syl323anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ∧ 𝑟𝐴 ∧ ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )
21 20 rexlimdv3a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) ∧ 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) )
22 21 3exp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) → ( 𝑃𝑄 → ( ¬ 𝑆 ( 𝑃 𝑄 ) → ( ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) ) ) )
23 22 3impd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ) → ( ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) ) )
24 23 3impia ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ ∃ 𝑟𝐴 ( ¬ 𝑟 𝑊 ∧ ( 𝑃 𝑟 ) = ( 𝑄 𝑟 ) ) ) ) → ∃ 𝑧𝐴 ( ¬ 𝑧 𝑊 ∧ ( 𝑃 𝑧 ) = ( 𝑆 𝑧 ) ) )