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 ( ( ( 𝐾𝐷𝑄𝐴𝑅𝐴 ) ∧ ( 𝑄𝑅𝑋 = { 𝑝𝐴𝑝 ( 𝑄 𝑅 ) } ) ) → 𝑋𝑁 )