Step |
Hyp |
Ref |
Expression |
1 |
|
dih1.m |
⊢ 1 = ( 1. ‘ 𝐾 ) |
2 |
|
dih1.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
3 |
|
dih1.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
dih1.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
dih1.v |
⊢ 𝑉 = ( Base ‘ 𝑈 ) |
6 |
2 3
|
dihvalrel |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 1 ) ) |
7 |
|
relxp |
⊢ Rel ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) |
8 |
|
eqid |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
9 |
|
eqid |
⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
10 |
2 8 9 4 5
|
dvhvbase |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑉 = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
11 |
10
|
releqd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Rel 𝑉 ↔ Rel ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
12 |
7 11
|
mpbiri |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel 𝑉 ) |
13 |
|
id |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
14 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝐾 ∈ OP ) |
16 |
|
simpl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
17 |
|
simprl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
18 |
|
simprr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) |
19 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
20 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
21 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
22 |
19 20 21 2
|
lhpocnel |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) |
23 |
22
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) |
24 |
|
eqid |
⊢ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) |
25 |
19 21 2 8 24
|
ltrniotacl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
26 |
16 23 23 25
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
27 |
2 8 9
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
28 |
16 18 26 27
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
29 |
2 8
|
ltrncnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
30 |
28 29
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
31 |
2 8
|
ltrnco |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
32 |
16 17 30 31
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
33 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
34 |
|
eqid |
⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
35 |
33 2 8 34
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ( Base ‘ 𝐾 ) ) |
36 |
32 35
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ( Base ‘ 𝐾 ) ) |
37 |
33 19 1
|
ople1 |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( le ‘ 𝐾 ) 1 ) |
38 |
15 36 37
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( le ‘ 𝐾 ) 1 ) |
39 |
38
|
ex |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( le ‘ 𝐾 ) 1 ) ) |
40 |
39
|
pm4.71d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( le ‘ 𝐾 ) 1 ) ) ) |
41 |
10
|
eleq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 〈 𝑓 , 𝑠 〉 ∈ 𝑉 ↔ 〈 𝑓 , 𝑠 〉 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
42 |
|
opelxp |
⊢ ( 〈 𝑓 , 𝑠 〉 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
43 |
41 42
|
bitrdi |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 〈 𝑓 , 𝑠 〉 ∈ 𝑉 ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
44 |
14
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP ) |
45 |
33 1
|
op1cl |
⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) ) |
46 |
44 45
|
syl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 1 ∈ ( Base ‘ 𝐾 ) ) |
47 |
|
hlpos |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset ) |
48 |
47
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ Poset ) |
49 |
33 2
|
lhpbase |
⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) ) |
50 |
49
|
adantl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) ) |
51 |
|
eqid |
⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 ) |
52 |
1 51 2
|
lhp1cvr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) 1 ) |
53 |
33 19 51
|
cvrnle |
⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 1 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑊 ( ⋖ ‘ 𝐾 ) 1 ) → ¬ 1 ( le ‘ 𝐾 ) 𝑊 ) |
54 |
48 50 46 52 53
|
syl31anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ¬ 1 ( le ‘ 𝐾 ) 𝑊 ) |
55 |
|
hlol |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL ) |
56 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
57 |
33 56 1
|
olm12 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 1 ( meet ‘ 𝐾 ) 𝑊 ) = 𝑊 ) |
58 |
55 49 57
|
syl2an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1 ( meet ‘ 𝐾 ) 𝑊 ) = 𝑊 ) |
59 |
58
|
oveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 1 ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) 𝑊 ) ) |
60 |
|
hllat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat ) |
61 |
60
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ Lat ) |
62 |
33 20
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) |
63 |
14 49 62
|
syl2an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) |
64 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
65 |
33 64
|
latjcom |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) 𝑊 ) = ( 𝑊 ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
66 |
61 63 50 65
|
syl3anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) 𝑊 ) = ( 𝑊 ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
67 |
33 20 64 1
|
opexmid |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑊 ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 1 ) |
68 |
14 49 67
|
syl2an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 1 ) |
69 |
59 66 68
|
3eqtrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 1 ( meet ‘ 𝐾 ) 𝑊 ) ) = 1 ) |
70 |
|
eqid |
⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) |
71 |
|
vex |
⊢ 𝑓 ∈ V |
72 |
|
vex |
⊢ 𝑠 ∈ V |
73 |
33 19 64 56 21 2 70 8 34 9 3 24 71 72
|
dihopelvalc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1 ∈ ( Base ‘ 𝐾 ) ∧ ¬ 1 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 1 ( meet ‘ 𝐾 ) 𝑊 ) ) = 1 ) ) → ( 〈 𝑓 , 𝑠 〉 ∈ ( 𝐼 ‘ 1 ) ↔ ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( le ‘ 𝐾 ) 1 ) ) ) |
74 |
13 46 54 22 69 73
|
syl122anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 〈 𝑓 , 𝑠 〉 ∈ ( 𝐼 ‘ 1 ) ↔ ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) ) ( le ‘ 𝐾 ) 1 ) ) ) |
75 |
40 43 74
|
3bitr4rd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 〈 𝑓 , 𝑠 〉 ∈ ( 𝐼 ‘ 1 ) ↔ 〈 𝑓 , 𝑠 〉 ∈ 𝑉 ) ) |
76 |
75
|
eqrelrdv2 |
⊢ ( ( ( Rel ( 𝐼 ‘ 1 ) ∧ Rel 𝑉 ) ∧ ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) → ( 𝐼 ‘ 1 ) = 𝑉 ) |
77 |
6 12 13 76
|
syl21anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 1 ) = 𝑉 ) |