Theorem linepmap

Description: A line described with a projective map. (Contributed by NM, 3-Feb-2012)

	Ref	Expression
Hypotheses	isline2.j	⊢ ∨ = ( join ‘ 𝐾 )
	isline2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	isline2.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
	isline2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	linepmap	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑀 ‘ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		isline2.j	⊢ ∨ = ( join ‘ 𝐾 )
2		isline2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		isline2.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
4		isline2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
5		simpl1	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ Lat )
6		simpl2	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝐴 )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 2	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9	6 8	syl	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10		simpl3	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ 𝐴 )
11	7 2	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12	10 11	syl	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13	7 1	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
14	5 9 12 13	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
15		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
16	7 15 2 4	pmapval	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ ( 𝑃 ∨ 𝑄 ) ) = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } )
17	5 14 16	syl2anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑀 ‘ ( 𝑃 ∨ 𝑄 ) ) = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } )
18		eqid	⊢ { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) }
19	15 1 2 3	islinei	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } = { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } ) ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } ∈ 𝑁 )
20	18 19	mpanr2	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) } ∈ 𝑁 )
21	17 20	eqeltrd	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑀 ‘ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝑁 )