Theorem isline4N

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isline4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isline4.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	isline4.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	isline4.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
	isline4.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	isline4N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 𝑝 𝐶 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		isline4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isline4.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		isline4.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		isline4.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
5		isline4.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
6		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7	1 6 3 4 5	isline3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
8		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
9	1 3	atbase	⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
10	9	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
11		simplr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
12		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13	1 12 6 2 3	cvrval3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑝 𝐶 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) = 𝑋 ) ) )
14	8 10 11 13	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 𝐶 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) = 𝑋 ) ) )
15		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
16	15	ad3antrrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
17		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
18		simplr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
19	12 3	atncmp	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ↔ 𝑞 ≠ 𝑝 ) )
20	16 17 18 19	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ↔ 𝑞 ≠ 𝑝 ) )
21		necom	⊢ ( 𝑞 ≠ 𝑝 ↔ 𝑝 ≠ 𝑞 )
22	20 21	bitrdi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ↔ 𝑝 ≠ 𝑞 ) )
23		eqcom	⊢ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) = 𝑋 ↔ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
24	23	a1i	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) = 𝑋 ↔ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) )
25	22 24	anbi12d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) = 𝑋 ) ↔ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
26	25	rexbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑝 ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) = 𝑋 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
27	14 26	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 𝐶 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
28	27	rexbidva	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 𝐶 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) )
29	7 28	bitr4d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 𝑝 𝐶 𝑋 ) )