This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dih1

Description: The value of isomorphism H at the lattice unity 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 ) = 𝑉 )