Metamath Proof Explorer


Theorem 2atjm

Description: The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012)

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

Proof

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