Metamath Proof Explorer

Theorem islinei

Description: Condition implying "is a line". (Contributed by NM, 3-Feb-2012)

Ref Expression
Hypotheses isline.l ⊢ ≤ = ( le ‘ 𝐾 )
isline.j ⊢ ∨ = ( join ‘ 𝐾 )
isline.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
isline.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
Assertion islinei ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → 𝑋 ∈ 𝑁 )

Proof

Step Hyp Ref Expression
1 isline.l ⊢ ≤ = ( le ‘ 𝐾 )
2 isline.j ⊢ ∨ = ( join ‘ 𝐾 )
3 isline.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 isline.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
5 simpl2 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → 𝑄 ∈ 𝐴 )
6 simpl3 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → 𝑅 ∈ 𝐴 )
7 simpr ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) )
8 neeq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ≠ 𝑟 ↔ 𝑄 ≠ 𝑟 ) )
9 oveq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) )
10 9 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) ) )
11 10 rabbidv ⊢ ( 𝑞 = 𝑄 → { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) } )
12 11 eqeq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ↔ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) } ) )
13 8 12 anbi12d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ( 𝑄 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) } ) ) )
14 neeq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑄 ≠ 𝑟 ↔ 𝑄 ≠ 𝑅 ) )
15 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑅 ) )
16 15 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) ) )
17 16 rabbidv ⊢ ( 𝑟 = 𝑅 → { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } )
18 17 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) } ↔ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) )
19 14 18 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑄 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑟 ) } ) ↔ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) )
20 13 19 rspc2ev ⊢ ( ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
21 5 6 7 20 syl3anc ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
22 simpl1 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → 𝐾 ∈ 𝐷 )
23 1 2 3 4 isline ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
24 22 23 syl ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
25 21 24 mpbird ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑄 ∨ 𝑅 ) } ) ) → 𝑋 ∈ 𝑁 )