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 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑝 ∈ 𝐴 𝑝 𝐶 𝑋 ) ) |