Step |
Hyp |
Ref |
Expression |
1 |
|
dihglblem.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
dihglblem.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
dihglblem.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
dihglblem.g |
⊢ 𝐺 = ( glb ‘ 𝐾 ) |
5 |
|
dihglblem.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
6 |
|
dihglblem.t |
⊢ 𝑇 = { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } |
7 |
|
dihglblem.i |
⊢ 𝐽 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
|
dihglblem.ih |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
9 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
10 |
|
simp11l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝐾 ∈ HL ) |
11 |
10
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝐾 ∈ Lat ) |
12 |
|
simp12l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 ) |
13 |
|
simp3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝑆 ) |
14 |
12 13
|
sseldd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝐵 ) |
15 |
|
simp11r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑊 ∈ 𝐻 ) |
16 |
1 5
|
lhpbase |
⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 ) |
17 |
15 16
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → 𝑊 ∈ 𝐵 ) |
18 |
1 2 3
|
latmle2 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑣 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 ) |
19 |
11 14 17 18
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 ) |
20 |
19
|
3expia |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑣 ∈ 𝑆 → ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 ) ) |
21 |
|
breq1 |
⊢ ( 𝑢 = ( 𝑣 ∧ 𝑊 ) → ( 𝑢 ≤ 𝑊 ↔ ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 ) ) |
22 |
21
|
biimprcd |
⊢ ( ( 𝑣 ∧ 𝑊 ) ≤ 𝑊 → ( 𝑢 = ( 𝑣 ∧ 𝑊 ) → 𝑢 ≤ 𝑊 ) ) |
23 |
20 22
|
syl6 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑣 ∈ 𝑆 → ( 𝑢 = ( 𝑣 ∧ 𝑊 ) → 𝑢 ≤ 𝑊 ) ) ) |
24 |
23
|
rexlimdv |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑢 ∈ 𝐵 ) → ( ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) → 𝑢 ≤ 𝑊 ) ) |
25 |
24
|
ss2rabdv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → { 𝑢 ∈ 𝐵 ∣ ∃ 𝑣 ∈ 𝑆 𝑢 = ( 𝑣 ∧ 𝑊 ) } ⊆ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ) |
26 |
6 25
|
eqsstrid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑇 ⊆ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ) |
27 |
1 2 5 7
|
dibdmN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐽 = { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ) |
28 |
27
|
3ad2ant1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → dom 𝐽 = { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ) |
29 |
26 28
|
sseqtrrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑇 ⊆ dom 𝐽 ) |
30 |
1 2 3 4 5 6
|
dihglblem2aN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑇 ≠ ∅ ) |
31 |
30
|
3adant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑇 ≠ ∅ ) |
32 |
4 5 7
|
dibglbN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑇 ⊆ dom 𝐽 ∧ 𝑇 ≠ ∅ ) ) → ( 𝐽 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐽 ‘ 𝑥 ) ) |
33 |
9 29 31 32
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐽 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐽 ‘ 𝑥 ) ) |
34 |
1 2 3 4 5 6
|
dihglblem2N |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) ) |
35 |
34
|
3adant2r |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ 𝑇 ) ) |
36 |
35
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑇 ) ) ) |
37 |
|
simpl1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
38 |
26
|
sselda |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ) |
39 |
|
breq1 |
⊢ ( 𝑢 = 𝑥 → ( 𝑢 ≤ 𝑊 ↔ 𝑥 ≤ 𝑊 ) ) |
40 |
39
|
elrab |
⊢ ( 𝑥 ∈ { 𝑢 ∈ 𝐵 ∣ 𝑢 ≤ 𝑊 } ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ) |
41 |
38 40
|
sylib |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ) |
42 |
1 2 5 8 7
|
dihvalb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) ) |
43 |
37 41 42
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐽 ‘ 𝑥 ) ) |
44 |
43
|
iineq2dv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) = ∩ 𝑥 ∈ 𝑇 ( 𝐽 ‘ 𝑥 ) ) |
45 |
33 36 44
|
3eqtr4rd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) ) |
46 |
|
simp1l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝐾 ∈ HL ) |
47 |
|
hlclat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat ) |
48 |
46 47
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝐾 ∈ CLat ) |
49 |
|
simp2l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑆 ⊆ 𝐵 ) |
50 |
1 4
|
clatglbcl |
⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) |
51 |
48 49 50
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) |
52 |
|
simp3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) |
53 |
1 2 5 8 7
|
dihvalb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) ) |
54 |
9 51 52 53
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐽 ‘ ( 𝐺 ‘ 𝑆 ) ) ) |
55 |
35
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑇 ) ) ) |
56 |
45 54 55
|
3eqtr2rd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑇 ) ) = ∩ 𝑥 ∈ 𝑇 ( 𝐼 ‘ 𝑥 ) ) |