This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islln3

Description: The predicate "is a lattice line". (Contributed by NM, 17-Jun-2012)

Ref Expression
Hypotheses islln3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
islln3.j ⊢ ∨ = ( join ‘ 𝐾 )
islln3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
islln3.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion islln3 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) ) )

Proof

Step Hyp Ref Expression
1 islln3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 islln3.j ⊢ ∨ = ( join ‘ 𝐾 )
3 islln3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 islln3.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
6 1 5 3 4 islln4 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
7 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
8 1 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
9 8 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
10 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 1 11 2 5 3 cvrval3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ∨ 𝑞 ) = 𝑋 ) ) )
13 7 9 10 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ∨ 𝑞 ) = 𝑋 ) ) )
14 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
15 14 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
16 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
17 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
18 11 3 atncmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ↔ 𝑞 ≠ 𝑝 ) )
19 15 16 17 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ↔ 𝑞 ≠ 𝑝 ) )
20 necom ⊢ ( 𝑞 ≠ 𝑝 ↔ 𝑝 ≠ 𝑞 )
21 19 20 bitrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ↔ 𝑝 ≠ 𝑞 ) )
22 eqcom ⊢ ( ( 𝑝 ∨ 𝑞 ) = 𝑋 ↔ 𝑋 = ( 𝑝 ∨ 𝑞 ) )
23 22 a1i ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ∨ 𝑞 ) = 𝑋 ↔ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) )
24 21 23 anbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ∨ 𝑞 ) = 𝑋 ) ↔ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) ) )
25 24 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ∨ 𝑞 ) = 𝑋 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) ) )
26 13 25 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) ) )
27 26 rexbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) ) )
28 6 27 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ∨ 𝑞 ) ) ) )