| 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 ) = 𝑉 ) |