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

Metamath Proof Explorer

Theorem isline2

Description: Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012)

Ref Expression
Hypotheses isline2.j ⊢ ∨ = ( join ‘ 𝐾 )
isline2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
isline2.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
isline2.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion isline2 ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isline2.j ⊢ ∨ = ( join ‘ 𝐾 )
2 isline2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 isline2.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
4 isline2.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 5 1 2 3 isline ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) } ) ) )
7 simpl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 2 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
10 9 ad2antrl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
11 8 2 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
12 11 ad2antll ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
13 8 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
14 7 10 12 13 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
15 8 5 2 4 pmapval ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) } )
16 14 15 syldan ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) } )
17 16 eqeq2d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑋 = ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) ↔ 𝑋 = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) } ) )
18 17 anbi2d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) } ) ) )
19 18 2rexbidva ⊢ ( 𝐾 ∈ Lat → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) } ) ) )
20 6 19 bitr4d ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) ) ) )