Metamath Proof Explorer

Theorem dihmeetlem4preN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihmeetlem4.l ⊢ ≤ = ( le ‘ 𝐾 )
dihmeetlem4.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihmeetlem4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihmeetlem4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetlem4.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.z ⊢ 0 = ( 0g ‘ 𝑈 )
dihmeetlem4.g ⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
dihmeetlem4.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem4.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion dihmeetlem4preN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 dihmeetlem4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem4.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihmeetlem4.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dihmeetlem4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dihmeetlem4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dihmeetlem4.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 dihmeetlem4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 dihmeetlem4.z ⊢ 0 = ( 0g ‘ 𝑈 )
9 dihmeetlem4.g ⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
10 dihmeetlem4.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
11 dihmeetlem4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
12 dihmeetlem4.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13 dihmeetlem4.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
14 dihmeetlem4.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
15 5 6 dihvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑄 ) )
16 relin1 ⊢ ( Rel ( 𝐼 ‘ 𝑄 ) → Rel ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
17 15 16 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
18 17 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → Rel ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
19 5 6 dihvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) )
20 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
21 20 5 6 7 8 dih0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
22 21 releqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Rel ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ Rel { 0 } ) )
23 19 22 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel { 0 } )
24 23 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → Rel { 0 } )
25 id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
26 elin ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
27 vex ⊢ 𝑓 ∈ V
28 vex ⊢ 𝑠 ∈ V
29 2 4 5 10 11 13 6 9 27 28 dihopelvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) )
30 29 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) )
31 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
33 32 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
34 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
35 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
36 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
37 35 36 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
38 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
39 33 34 37 38 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
40 1 2 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
41 33 34 37 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
42 1 2 5 11 12 14 6 dihopelvalbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) )
43 31 39 41 42 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) )
44 30 43 anbi12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) )
45 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → 𝑓 = ( 𝑠 ‘ 𝐺 ) )
46 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → 𝑠 = 𝑂 )
47 46 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → ( 𝑠 ‘ 𝐺 ) = ( 𝑂 ‘ 𝐺 ) )
48 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
49 2 4 5 10 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
50 48 49 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
51 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
52 2 4 5 11 9 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
53 48 50 51 52 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → 𝐺 ∈ 𝑇 )
54 14 1 tendo02 ⊢ ( 𝐺 ∈ 𝑇 → ( 𝑂 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
55 53 54 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → ( 𝑂 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
56 45 47 55 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → 𝑓 = ( I ↾ 𝐵 ) )
57 56 46 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ) → ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) )
58 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
59 58 49 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
60 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
61 58 59 60 52 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝐺 ∈ 𝑇 )
62 61 54 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑂 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
63 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝑠 = 𝑂 )
64 63 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑠 ‘ 𝐺 ) = ( 𝑂 ‘ 𝐺 ) )
65 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝑓 = ( I ↾ 𝐵 ) )
66 62 64 65 3eqtr4rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝑓 = ( 𝑠 ‘ 𝐺 ) )
67 1 5 11 13 14 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
68 58 67 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝑂 ∈ 𝐸 )
69 63 68 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝑠 ∈ 𝐸 )
70 1 5 11 idltrn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
71 58 70 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
72 65 71 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝑓 ∈ 𝑇 )
73 65 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑅 ‘ 𝑓 ) = ( 𝑅 ‘ ( I ↾ 𝐵 ) ) )
74 1 20 5 12 trlid0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) )
75 58 74 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑅 ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) )
76 73 75 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑅 ‘ 𝑓 ) = ( 0. ‘ 𝐾 ) )
77 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝐾 ∈ HL )
78 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
79 77 78 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → 𝐾 ∈ AtLat )
80 39 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
81 1 2 20 atl0le ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 0. ‘ 𝐾 ) ≤ ( 𝑋 ∧ 𝑊 ) )
82 79 80 81 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 0. ‘ 𝐾 ) ≤ ( 𝑋 ∧ 𝑊 ) )
83 76 82 eqbrtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) )
84 72 83 63 jca31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) )
85 66 69 84 jca31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) → ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) )
86 57 85 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑠 = 𝑂 ) ) ↔ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) )
87 44 86 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) )
88 opex ⊢ ⟨ 𝑓 , 𝑠 ⟩ ∈ V
89 88 elsn ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } ↔ ⟨ 𝑓 , 𝑠 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
90 27 28 opth ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ↔ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) )
91 89 90 bitr2i ⊢ ( ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } )
92 87 91 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } ) )
93 1 5 11 7 8 14 dvh0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
94 93 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
95 94 sneqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → { 0 } = { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } )
96 95 eleq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ { 0 } ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } ) )
97 92 96 bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { 0 } ) )
98 26 97 syl5bb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { 0 } ) )
99 98 eqrelrdv2 ⊢ ( ( ( Rel ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ Rel { 0 } ) ∧ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = { 0 } )
100 18 24 25 99 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = { 0 } )