Step |
Hyp |
Ref |
Expression |
1 |
|
pexmidlem.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
pexmidlem.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
pexmidlem.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
pexmidlem.p |
⊢ + = ( +𝑃 ‘ 𝐾 ) |
5 |
|
pexmidlem.o |
⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 ) |
6 |
|
pexmidlem.m |
⊢ 𝑀 = ( 𝑋 + { 𝑝 } ) |
7 |
1 2 3 4 5 6
|
pexmidlem5N |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) = ∅ ) |
8 |
7
|
3adantr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) = ∅ ) |
9 |
8
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) = ( ⊥ ‘ ∅ ) ) |
10 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝐾 ∈ HL ) |
11 |
3 5
|
pol0N |
⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ∅ ) = 𝐴 ) |
12 |
10 11
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ⊥ ‘ ∅ ) = 𝐴 ) |
13 |
9 12
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) = 𝐴 ) |
14 |
13
|
ineq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) ∩ 𝑀 ) = ( 𝐴 ∩ 𝑀 ) ) |
15 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑋 ⊆ 𝐴 ) |
16 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑝 ∈ 𝐴 ) |
17 |
16
|
snssd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → { 𝑝 } ⊆ 𝐴 ) |
18 |
3 4
|
paddssat |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ { 𝑝 } ⊆ 𝐴 ) → ( 𝑋 + { 𝑝 } ) ⊆ 𝐴 ) |
19 |
10 15 17 18
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 + { 𝑝 } ) ⊆ 𝐴 ) |
20 |
6 19
|
eqsstrid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑀 ⊆ 𝐴 ) |
21 |
10 15 20
|
3jca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑀 ⊆ 𝐴 ) ) |
22 |
3 4
|
sspadd1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ { 𝑝 } ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + { 𝑝 } ) ) |
23 |
10 15 17 22
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑋 ⊆ ( 𝑋 + { 𝑝 } ) ) |
24 |
23 6
|
sseqtrrdi |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑋 ⊆ 𝑀 ) |
25 |
|
simpr1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) |
26 |
|
eqid |
⊢ ( PSubCl ‘ 𝐾 ) = ( PSubCl ‘ 𝐾 ) |
27 |
3 5 26
|
ispsubclN |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) ) |
28 |
10 27
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) ) |
29 |
15 25 28
|
mpbir2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ) |
30 |
3 4 26
|
paddatclN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( PSubCl ‘ 𝐾 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑋 + { 𝑝 } ) ∈ ( PSubCl ‘ 𝐾 ) ) |
31 |
10 29 16 30
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 + { 𝑝 } ) ∈ ( PSubCl ‘ 𝐾 ) ) |
32 |
6 31
|
eqeltrid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑀 ∈ ( PSubCl ‘ 𝐾 ) ) |
33 |
5 26
|
psubcli2N |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑀 ∈ ( PSubCl ‘ 𝐾 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑀 ) ) = 𝑀 ) |
34 |
10 32 33
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑀 ) ) = 𝑀 ) |
35 |
24 34
|
jca |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 ⊆ 𝑀 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑀 ) ) = 𝑀 ) ) |
36 |
3 5
|
poml4N |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑀 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑀 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑀 ) ) = 𝑀 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) ∩ 𝑀 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ) |
37 |
21 35 36
|
sylc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ) ∩ 𝑀 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) |
38 |
|
sseqin2 |
⊢ ( 𝑀 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑀 ) = 𝑀 ) |
39 |
20 38
|
sylib |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝐴 ∩ 𝑀 ) = 𝑀 ) |
40 |
14 37 39
|
3eqtr3rd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑀 = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) |
41 |
40 25
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑀 = 𝑋 ) |