Metamath Proof Explorer


Theorem cdleme46f2g2

Description: Conversion for G to reuse F theorems. TODO FIX COMMENT. TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq ? Find other hlatjcom uses giving Q .\/ P . (Contributed by NM, 1-Apr-2013)

Ref Expression
Hypotheses cdleme46fg.j = ( join ‘ 𝐾 )
cdleme46fg.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cdleme46f2g2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝑄𝑃 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑄 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cdleme46fg.j = ( join ‘ 𝐾 )
2 cdleme46fg.a 𝐴 = ( Atoms ‘ 𝐾 )
3 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
4 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
5 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
6 3 4 5 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) )
7 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑃𝑄 )
8 7 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → 𝑄𝑃 )
9 simp2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) )
10 8 9 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( 𝑄𝑃 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) )
11 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ) → 𝐾 ∈ HL )
12 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ) → 𝑃𝐴 )
13 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ) → 𝑄𝐴 )
14 1 2 hlatjcom ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) = ( 𝑄 𝑃 ) )
15 11 12 13 14 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑄 𝑃 ) )
16 15 breq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ) → ( 𝑆 ( 𝑃 𝑄 ) ↔ 𝑆 ( 𝑄 𝑃 ) ) )
17 16 notbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ) → ( ¬ 𝑆 ( 𝑃 𝑄 ) ↔ ¬ 𝑆 ( 𝑄 𝑃 ) ) )
18 17 biimp3a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ¬ 𝑆 ( 𝑄 𝑃 ) )
19 6 10 18 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝑄𝑃 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑄 𝑃 ) ) )