Step |
Hyp |
Ref |
Expression |
1 |
|
dihoml4c.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dihoml4c.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
dihoml4c.o |
⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
dihoml4c.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
5 |
|
dihoml4c.x |
⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 ) |
6 |
|
dihoml4c.y |
⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 ) |
7 |
|
dihoml4c.l |
⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 ) |
8 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
9 |
|
inss1 |
⊢ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) |
10 |
|
eqid |
⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
11 |
|
eqid |
⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) |
12 |
1 10 2 11
|
dihrnss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
13 |
4 5 12
|
syl2anc |
⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
14 |
1 10 11 3
|
dochssv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
15 |
4 13 14
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
16 |
9 15
|
sstrid |
⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
17 |
1 2 10 11 3
|
dochcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∈ ran 𝐼 ) |
18 |
4 16 17
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∈ ran 𝐼 ) |
19 |
8 1 2 4 18 6
|
dihmeet2 |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) |
20 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
21 |
1 2 10 11 3
|
dochcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 ) |
22 |
4 13 21
|
syl2anc |
⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 ) |
23 |
1 2
|
dihmeetcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ∈ ran 𝐼 ) |
24 |
4 22 6 23
|
syl12anc |
⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ∈ ran 𝐼 ) |
25 |
20 1 2 3 4 24
|
dochvalr3 |
⊢ ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ) = ( ◡ 𝐼 ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ) ) |
26 |
8 1 2 4 22 6
|
dihmeet2 |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ ( ⊥ ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) |
27 |
20 1 2 3 4 5
|
dochvalr3 |
⊢ ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( ◡ 𝐼 ‘ ( ⊥ ‘ 𝑋 ) ) ) |
28 |
27
|
oveq1d |
⊢ ( 𝜑 → ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ ( ⊥ ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) |
29 |
26 28
|
eqtr4d |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) |
30 |
29
|
fveq2d |
⊢ ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ) |
31 |
25 30
|
eqtr3d |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ) |
32 |
31
|
oveq1d |
⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) |
33 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
34 |
33 1 2 4 5 6
|
dihcnvord |
⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) ) |
35 |
7 34
|
mpbird |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) |
36 |
4
|
simpld |
⊢ ( 𝜑 → 𝐾 ∈ HL ) |
37 |
|
hloml |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OML ) |
38 |
36 37
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ OML ) |
39 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
40 |
39 1 2
|
dihcnvcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) |
41 |
4 5 40
|
syl2anc |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) |
42 |
39 1 2
|
dihcnvcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) |
43 |
4 6 42
|
syl2anc |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) |
44 |
39 33 8 20
|
omllaw4 |
⊢ ( ( 𝐾 ∈ OML ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) ) ) |
45 |
38 41 43 44
|
syl3anc |
⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) ) ) |
46 |
35 45
|
mpd |
⊢ ( 𝜑 → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) ) |
47 |
19 32 46
|
3eqtrd |
⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) ) |
48 |
1 2
|
dihmeetcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ∈ ran 𝐼 ) |
49 |
4 18 6 48
|
syl12anc |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ∈ ran 𝐼 ) |
50 |
1 2 4 49 5
|
dihcnv11 |
⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) ↔ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 ) ) |
51 |
47 50
|
mpbid |
⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 ) |