Metamath Proof Explorer


Theorem 2llnma1b

Description: Generalization of 2llnma1 . (Contributed by NM, 26-Apr-2013)

Ref Expression
Hypotheses 2llnma1b.b 𝐵 = ( Base ‘ 𝐾 )
2llnma1b.l = ( le ‘ 𝐾 )
2llnma1b.j = ( join ‘ 𝐾 )
2llnma1b.m = ( meet ‘ 𝐾 )
2llnma1b.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2llnma1b ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) = 𝑃 )

Proof

Step Hyp Ref Expression
1 2llnma1b.b 𝐵 = ( Base ‘ 𝐾 )
2 2llnma1b.l = ( le ‘ 𝐾 )
3 2llnma1b.j = ( join ‘ 𝐾 )
4 2llnma1b.m = ( meet ‘ 𝐾 )
5 2llnma1b.a 𝐴 = ( Atoms ‘ 𝐾 )
6 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 6 3ad2ant1 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝐾 ∈ Lat )
8 simp22 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃𝐴 )
9 1 5 atbase ( 𝑃𝐴𝑃𝐵 )
10 8 9 syl ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃𝐵 )
11 simp21 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑋𝐵 )
12 1 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵 ) → 𝑃 ( 𝑃 𝑋 ) )
13 7 10 11 12 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃 ( 𝑃 𝑋 ) )
14 simp23 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑄𝐴 )
15 1 5 atbase ( 𝑄𝐴𝑄𝐵 )
16 14 15 syl ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑄𝐵 )
17 1 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵 ) → 𝑃 ( 𝑃 𝑄 ) )
18 7 10 16 17 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃 ( 𝑃 𝑄 ) )
19 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵 ) → ( 𝑃 𝑋 ) ∈ 𝐵 )
20 7 10 11 19 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( 𝑃 𝑋 ) ∈ 𝐵 )
21 simp1 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝐾 ∈ HL )
22 1 3 5 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ 𝐵 )
23 21 8 14 22 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( 𝑃 𝑄 ) ∈ 𝐵 )
24 1 2 4 latlem12 ( ( 𝐾 ∈ Lat ∧ ( 𝑃𝐵 ∧ ( 𝑃 𝑋 ) ∈ 𝐵 ∧ ( 𝑃 𝑄 ) ∈ 𝐵 ) ) → ( ( 𝑃 ( 𝑃 𝑋 ) ∧ 𝑃 ( 𝑃 𝑄 ) ) ↔ 𝑃 ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ) )
25 7 10 20 23 24 syl13anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( ( 𝑃 ( 𝑃 𝑋 ) ∧ 𝑃 ( 𝑃 𝑄 ) ) ↔ 𝑃 ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ) )
26 13 18 25 mpbi2and ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃 ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) )
27 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
28 27 3ad2ant1 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝐾 ∈ AtLat )
29 simp3 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ¬ 𝑄 ( 𝑃 𝑋 ) )
30 nbrne2 ( ( 𝑃 ( 𝑃 𝑋 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃𝑄 )
31 13 29 30 syl2anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃𝑄 )
32 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑋 ) ∈ 𝐵𝑄𝐵 ) → ( ( 𝑃 𝑋 ) 𝑄 ) ∈ 𝐵 )
33 7 20 16 32 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( ( 𝑃 𝑋 ) 𝑄 ) ∈ 𝐵 )
34 1 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑋 ) ∈ 𝐵𝑄𝐵 ) → ( 𝑃 𝑋 ) ( ( 𝑃 𝑋 ) 𝑄 ) )
35 7 20 16 34 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( 𝑃 𝑋 ) ( ( 𝑃 𝑋 ) 𝑄 ) )
36 1 2 7 10 20 33 13 35 lattrd ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃 ( ( 𝑃 𝑋 ) 𝑄 ) )
37 1 2 3 4 5 cvrat3 ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 𝑋 ) ∈ 𝐵𝑃𝐴𝑄𝐴 ) ) → ( ( 𝑃𝑄 ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ∧ 𝑃 ( ( 𝑃 𝑋 ) 𝑄 ) ) → ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ∈ 𝐴 ) )
38 37 3impia ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 𝑋 ) ∈ 𝐵𝑃𝐴𝑄𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ∧ 𝑃 ( ( 𝑃 𝑋 ) 𝑄 ) ) ) → ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ∈ 𝐴 )
39 21 20 8 14 31 29 36 38 syl133anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ∈ 𝐴 )
40 2 5 atcmp ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴 ∧ ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ∈ 𝐴 ) → ( 𝑃 ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ↔ 𝑃 = ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ) )
41 28 8 39 40 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( 𝑃 ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ↔ 𝑃 = ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) ) )
42 26 41 mpbid ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → 𝑃 = ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) )
43 42 eqcomd ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑄 ( 𝑃 𝑋 ) ) → ( ( 𝑃 𝑋 ) ( 𝑃 𝑄 ) ) = 𝑃 )