Metamath Proof Explorer

Theorem dihmeetlem13N

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

Ref Expression
Hypotheses dihmeetlem13.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihmeetlem13.l ⊢ ≤ = ( le ‘ 𝐾 )
dihmeetlem13.j ⊢ ∨ = ( join ‘ 𝐾 )
dihmeetlem13.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihmeetlem13.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetlem13.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem13.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem13.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem13.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dihmeetlem13.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem13.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem13.z ⊢ 0 = ( 0g ‘ 𝑈 )
dihmeetlem13.f ⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
dihmeetlem13.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
Assertion dihmeetlem13N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 dihmeetlem13.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem13.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihmeetlem13.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dihmeetlem13.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dihmeetlem13.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dihmeetlem13.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
7 dihmeetlem13.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 dihmeetlem13.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
9 dihmeetlem13.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
10 dihmeetlem13.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
11 dihmeetlem13.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
12 dihmeetlem13.z ⊢ 0 = ( 0g ‘ 𝑈 )
13 dihmeetlem13.f ⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
14 dihmeetlem13.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
15 5 10 dihvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑄 ) )
16 15 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → Rel ( 𝐼 ‘ 𝑄 ) )
17 relin1 ⊢ ( Rel ( 𝐼 ‘ 𝑄 ) → Rel ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) )
18 16 17 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → Rel ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) )
19 elin ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) ↔ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑅 ) ) )
20 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
22 vex ⊢ 𝑓 ∈ V
23 vex ⊢ 𝑠 ∈ V
24 2 4 5 6 7 8 10 13 22 23 dihopelvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ) )
25 20 21 24 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ) )
26 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
27 2 4 5 6 7 8 10 14 22 23 dihopelvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑅 ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) )
28 20 26 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑅 ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) )
29 25 28 anbi12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑅 ) ) ↔ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) )
30 19 29 bitrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) ↔ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) )
31 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → 𝑓 = ( 𝑠 ‘ 𝐹 ) )
32 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → 𝑄 ≠ 𝑅 )
33 fveq1 ⊢ ( 𝐹 = 𝐺 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) )
34 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35 2 4 5 6 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
36 34 35 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
37 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
38 2 4 5 7 13 ltrniotaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑄 )
39 34 36 37 38 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑄 )
40 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
41 2 4 5 7 14 ltrniotaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝑃 ) = 𝑅 )
42 34 36 40 41 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝐺 ‘ 𝑃 ) = 𝑅 )
43 39 42 eqeq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ↔ 𝑄 = 𝑅 ) )
44 33 43 imbitrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝐹 = 𝐺 → 𝑄 = 𝑅 ) )
45 44 necon3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑄 ≠ 𝑅 → 𝐹 ≠ 𝐺 ) )
46 32 45 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → 𝐹 ≠ 𝐺 )
47 simp2ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑓 = ( 𝑠 ‘ 𝐹 ) )
48 simp2rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑓 = ( 𝑠 ‘ 𝐺 ) )
49 47 48 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑠 ‘ 𝐹 ) = ( 𝑠 ‘ 𝐺 ) )
50 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
51 simp2rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑠 ∈ 𝐸 )
52 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑠 ≠ 𝑂 )
53 50 35 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
54 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
55 2 4 5 7 13 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
56 50 53 54 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝐹 ∈ 𝑇 )
57 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
58 2 4 5 7 14 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
59 50 53 57 58 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝐺 ∈ 𝑇 )
60 1 5 7 8 9 tendospcanN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑠 ‘ 𝐹 ) = ( 𝑠 ‘ 𝐺 ) ↔ 𝐹 = 𝐺 ) )
61 50 51 52 56 59 60 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑠 ‘ 𝐹 ) = ( 𝑠 ‘ 𝐺 ) ↔ 𝐹 = 𝐺 ) )
62 49 61 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝐹 = 𝐺 )
63 62 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑠 ≠ 𝑂 → 𝐹 = 𝐺 ) )
64 63 necon1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝐹 ≠ 𝐺 → 𝑠 = 𝑂 ) )
65 46 64 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → 𝑠 = 𝑂 )
66 65 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑠 ‘ 𝐹 ) = ( 𝑂 ‘ 𝐹 ) )
67 34 36 37 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → 𝐹 ∈ 𝑇 )
68 9 1 tendo02 ⊢ ( 𝐹 ∈ 𝑇 → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )
69 67 68 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑂 ‘ 𝐹 ) = ( I ↾ 𝐵 ) )
70 31 66 69 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → 𝑓 = ( I ↾ 𝐵 ) )
71 70 65 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) ∧ ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) → ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) )
72 71 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( ( 𝑓 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) )
73 30 72 sylbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) → ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ) )
74 opex ⊢ ⟨ 𝑓 , 𝑠 ⟩ ∈ V
75 74 elsn ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } ↔ ⟨ 𝑓 , 𝑠 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
76 22 23 opth ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ↔ ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) )
77 75 76 bitr2i ⊢ ( ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } )
78 1 5 7 11 12 9 dvh0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
79 78 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
80 79 sneqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → { 0 } = { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } )
81 80 eleq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ { 0 } ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ } ) )
82 77 81 bitr4id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( 𝑓 = ( I ↾ 𝐵 ) ∧ 𝑠 = 𝑂 ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ { 0 } ) )
83 73 82 sylibd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ { 0 } ) )
84 18 83 relssdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) ⊆ { 0 } )
85 5 11 20 dvhlmod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑈 ∈ LMod )
86 simp2ll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑄 ∈ 𝐴 )
87 1 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
88 86 87 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑄 ∈ 𝐵 )
89 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
90 1 5 10 11 89 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
91 20 88 90 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝐼 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
92 simp2rl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑅 ∈ 𝐴 )
93 1 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
94 92 93 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → 𝑅 ∈ 𝐵 )
95 1 5 10 11 89 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑅 ) ∈ ( LSubSp ‘ 𝑈 ) )
96 20 94 95 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( 𝐼 ‘ 𝑅 ) ∈ ( LSubSp ‘ 𝑈 ) )
97 89 lssincl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( 𝐼 ‘ 𝑅 ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
98 85 91 96 97 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
99 12 89 lss0ss ⊢ ( ( 𝑈 ∈ LMod ∧ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) → { 0 } ⊆ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) )
100 85 98 99 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → { 0 } ⊆ ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) )
101 84 100 eqssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝑄 ≠ 𝑅 ) → ( ( 𝐼 ‘ 𝑄 ) ∩ ( 𝐼 ‘ 𝑅 ) ) = { 0 } )