Metamath Proof Explorer


Theorem dih1

Description: The value of isomorphism H at the lattice unit is the set of all vectors. (Contributed by NM, 13-Mar-2014)

Ref Expression
Hypotheses dih1.m 1 = ( 1. ‘ 𝐾 )
dih1.h 𝐻 = ( LHyp ‘ 𝐾 )
dih1.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih1.v 𝑉 = ( Base ‘ 𝑈 )
Assertion dih1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐼1 ) = 𝑉 )

Proof

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