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 → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑀 ‘ ( 𝑝 ∨ 𝑞 ) ) ) ) )