Metamath Proof Explorer


Theorem llni2

Description: The join of two different atoms is a lattice line. (Contributed by NM, 26-Jun-2012)

Ref Expression
Hypotheses llni2.j = ( join ‘ 𝐾 )
llni2.a 𝐴 = ( Atoms ‘ 𝐾 )
llni2.n 𝑁 = ( LLines ‘ 𝐾 )
Assertion llni2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑃 𝑄 ) ∈ 𝑁 )

Proof

Step Hyp Ref Expression
1 llni2.j = ( join ‘ 𝐾 )
2 llni2.a 𝐴 = ( Atoms ‘ 𝐾 )
3 llni2.n 𝑁 = ( LLines ‘ 𝐾 )
4 simpl2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → 𝑃𝐴 )
5 simpl3 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → 𝑄𝐴 )
6 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → 𝑃𝑄 )
7 eqidd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑃 𝑄 ) = ( 𝑃 𝑄 ) )
8 neeq1 ( 𝑟 = 𝑃 → ( 𝑟𝑠𝑃𝑠 ) )
9 oveq1 ( 𝑟 = 𝑃 → ( 𝑟 𝑠 ) = ( 𝑃 𝑠 ) )
10 9 eqeq2d ( 𝑟 = 𝑃 → ( ( 𝑃 𝑄 ) = ( 𝑟 𝑠 ) ↔ ( 𝑃 𝑄 ) = ( 𝑃 𝑠 ) ) )
11 8 10 anbi12d ( 𝑟 = 𝑃 → ( ( 𝑟𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑟 𝑠 ) ) ↔ ( 𝑃𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑃 𝑠 ) ) ) )
12 neeq2 ( 𝑠 = 𝑄 → ( 𝑃𝑠𝑃𝑄 ) )
13 oveq2 ( 𝑠 = 𝑄 → ( 𝑃 𝑠 ) = ( 𝑃 𝑄 ) )
14 13 eqeq2d ( 𝑠 = 𝑄 → ( ( 𝑃 𝑄 ) = ( 𝑃 𝑠 ) ↔ ( 𝑃 𝑄 ) = ( 𝑃 𝑄 ) ) )
15 12 14 anbi12d ( 𝑠 = 𝑄 → ( ( 𝑃𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑃 𝑠 ) ) ↔ ( 𝑃𝑄 ∧ ( 𝑃 𝑄 ) = ( 𝑃 𝑄 ) ) ) )
16 11 15 rspc2ev ( ( 𝑃𝐴𝑄𝐴 ∧ ( 𝑃𝑄 ∧ ( 𝑃 𝑄 ) = ( 𝑃 𝑄 ) ) ) → ∃ 𝑟𝐴𝑠𝐴 ( 𝑟𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑟 𝑠 ) ) )
17 4 5 6 7 16 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ∃ 𝑟𝐴𝑠𝐴 ( 𝑟𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑟 𝑠 ) ) )
18 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → 𝐾 ∈ HL )
19 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 1 2 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
21 20 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
22 19 1 2 3 islln3 ( ( 𝐾 ∈ HL ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) ∈ 𝑁 ↔ ∃ 𝑟𝐴𝑠𝐴 ( 𝑟𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑟 𝑠 ) ) ) )
23 18 21 22 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( ( 𝑃 𝑄 ) ∈ 𝑁 ↔ ∃ 𝑟𝐴𝑠𝐴 ( 𝑟𝑠 ∧ ( 𝑃 𝑄 ) = ( 𝑟 𝑠 ) ) ) )
24 17 23 mpbird ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑃 𝑄 ) ∈ 𝑁 )