Metamath Proof Explorer

Theorem dih1dimatlem

Description: Lemma for dih1dimat . (Contributed by NM, 10-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dih1dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dih1dimat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dih1dimat.l ⊢ ≤ = ( le ‘ 𝐾 )
dih1dimat.c ⊢ 𝐶 = ( Atoms ‘ 𝐾 )
dih1dimat.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dih1dimat.d ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
dih1dimat.j ⊢ 𝐽 = ( invr ‘ 𝐹 )
dih1dimat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dih1dimat.m ⊢ · = ( ·𝑠 ‘ 𝑈 )
dih1dimat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dih1dimat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dih1dimat.z ⊢ 0 = ( 0g ‘ 𝑈 )
dih1dimat.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) )
Assertion dih1dimatlem ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝐴 ) → 𝐷 ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dih1dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dih1dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dih1dimat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dih1dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5 dih1dimat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
6 dih1dimat.l ⊢ ≤ = ( le ‘ 𝐾 )
7 dih1dimat.c ⊢ 𝐶 = ( Atoms ‘ 𝐾 )
8 dih1dimat.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
9 dih1dimat.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10 dih1dimat.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11 dih1dimat.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12 dih1dimat.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
13 dih1dimat.d ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
14 dih1dimat.j ⊢ 𝐽 = ( invr ‘ 𝐹 )
15 dih1dimat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
16 dih1dimat.m ⊢ · = ( ·𝑠 ‘ 𝑈 )
17 dih1dimat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
18 dih1dimat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
19 dih1dimat.z ⊢ 0 = ( 0g ‘ 𝑈 )
20 dih1dimat.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) )
21 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22 1 2 21 dvhlvec ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )
23 15 18 19 4 islsat ⊢ ( 𝑈 ∈ LVec → ( 𝐷 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) 𝐷 = ( 𝑁 ‘ { 𝑣 } ) ) )
24 22 23 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐷 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) 𝐷 = ( 𝑁 ‘ { 𝑣 } ) ) )
25 24 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝐴 ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) 𝐷 = ( 𝑁 ‘ { 𝑣 } ) )
26 eldifi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) → 𝑣 ∈ 𝑉 )
27 1 9 11 2 15 dvhvbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑉 = ( 𝑇 × 𝐸 ) )
28 27 eleq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑣 ∈ 𝑉 ↔ 𝑣 ∈ ( 𝑇 × 𝐸 ) ) )
29 26 28 syl5ib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑣 ∈ ( 𝑉 ∖ { 0 } ) → 𝑣 ∈ ( 𝑇 × 𝐸 ) ) )
30 29 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑣 ∈ ( 𝑇 × 𝐸 ) )
31 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 = 𝑂 ) → 𝑠 = 𝑂 )
32 31 opeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 = 𝑂 ) → ⟨ 𝑓 , 𝑠 ⟩ = ⟨ 𝑓 , 𝑂 ⟩ )
33 32 sneqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 = 𝑂 ) → { ⟨ 𝑓 , 𝑠 ⟩ } = { ⟨ 𝑓 , 𝑂 ⟩ } )
34 33 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 = 𝑂 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
35 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
36 5 1 9 10 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 )
37 6 1 9 10 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑊 )
38 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
39 5 6 1 3 38 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝑓 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝑓 ) ) )
40 35 36 37 39 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝑓 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝑓 ) ) )
41 5 1 9 10 12 2 38 18 dib1dim2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝑓 ) ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
42 40 41 eqtr2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑓 ) ) )
43 5 1 3 2 17 dihf11 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 –1-1→ 𝑆 )
44 43 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → 𝐼 : 𝐵 –1-1→ 𝑆 )
45 f1fn ⊢ ( 𝐼 : 𝐵 –1-1→ 𝑆 → 𝐼 Fn 𝐵 )
46 44 45 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → 𝐼 Fn 𝐵 )
47 fnfvelrn ⊢ ( ( 𝐼 Fn 𝐵 ∧ ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝑓 ) ) ∈ ran 𝐼 )
48 46 36 47 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝑓 ) ) ∈ ran 𝐼 )
49 42 48 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ∈ ran 𝐼 )
50 49 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ∈ ran 𝐼 )
51 50 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 = 𝑂 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ∈ ran 𝐼 )
52 34 51 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 = 𝑂 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) ∈ ran 𝐼 )
53 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
54 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
55 1 11 2 13 54 dvhbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐹 ) = 𝐸 )
56 53 55 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( Base ‘ 𝐹 ) = 𝐸 )
57 56 rexeqdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ↔ ∃ 𝑡 ∈ 𝐸 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ) )
58 simplll ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
59 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → 𝑡 ∈ 𝐸 )
60 opelxpi ⊢ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝑇 × 𝐸 ) )
61 60 ad3antlr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝑇 × 𝐸 ) )
62 1 9 11 2 16 dvhvscacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ∈ ( 𝑇 × 𝐸 ) )
63 58 59 61 62 syl12anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ∈ ( 𝑇 × 𝐸 ) )
64 eleq1a ⊢ ( ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ∈ ( 𝑇 × 𝐸 ) → ( 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) → 𝑢 ∈ ( 𝑇 × 𝐸 ) ) )
65 63 64 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) → 𝑢 ∈ ( 𝑇 × 𝐸 ) ) )
66 65 rexlimdva ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ∃ 𝑡 ∈ 𝐸 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) → 𝑢 ∈ ( 𝑇 × 𝐸 ) ) )
67 66 pm4.71rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ∃ 𝑡 ∈ 𝐸 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ↔ ( 𝑢 ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ) ) )
68 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑓 ∈ 𝑇 )
69 68 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → 𝑓 ∈ 𝑇 )
70 simplrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑠 ∈ 𝐸 )
71 70 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → 𝑠 ∈ 𝐸 )
72 1 9 11 2 16 dvhopvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ )
73 58 59 69 71 72 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ )
74 73 eqeq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ↔ 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) )
75 74 rexbidva ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ∃ 𝑡 ∈ 𝐸 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ↔ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) )
76 75 anbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑢 ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ) ↔ ( 𝑢 ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) ) )
77 57 67 76 3bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) ↔ ( 𝑢 ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) ) )
78 77 abbidv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → { 𝑢 ∣ ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) } = { 𝑢 ∣ ( 𝑢 ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) } )
79 df-rab ⊢ { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } = { 𝑢 ∣ ( 𝑢 ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) }
80 78 79 eqtr4di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → { 𝑢 ∣ ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) } = { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } )
81 ssrab2 ⊢ { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } ⊆ ( 𝑇 × 𝐸 )
82 relxp ⊢ Rel ( 𝑇 × 𝐸 )
83 relss ⊢ ( { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } ⊆ ( 𝑇 × 𝐸 ) → ( Rel ( 𝑇 × 𝐸 ) → Rel { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } ) )
84 81 82 83 mp2 ⊢ Rel { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ }
85 relopabv ⊢ Rel { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) }
86 vex ⊢ 𝑖 ∈ V
87 vex ⊢ 𝑝 ∈ V
88 eqeq1 ⊢ ( 𝑔 = 𝑖 → ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ↔ 𝑖 = ( 𝑟 ‘ 𝐺 ) ) )
89 88 anbi1d ⊢ ( 𝑔 = 𝑖 → ( ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) ↔ ( 𝑖 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) ) )
90 fveq1 ⊢ ( 𝑟 = 𝑝 → ( 𝑟 ‘ 𝐺 ) = ( 𝑝 ‘ 𝐺 ) )
91 90 eqeq2d ⊢ ( 𝑟 = 𝑝 → ( 𝑖 = ( 𝑟 ‘ 𝐺 ) ↔ 𝑖 = ( 𝑝 ‘ 𝐺 ) ) )
92 eleq1w ⊢ ( 𝑟 = 𝑝 → ( 𝑟 ∈ 𝐸 ↔ 𝑝 ∈ 𝐸 ) )
93 91 92 anbi12d ⊢ ( 𝑟 = 𝑝 → ( ( 𝑖 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) ↔ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) )
94 86 87 89 93 opelopab ⊢ ( ⟨ 𝑖 , 𝑝 ⟩ ∈ { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } ↔ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) )
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ↔ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) )
96 95 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ↔ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) )
97 opelxp ⊢ ( ⟨ 𝑖 , 𝑝 ⟩ ∈ ( 𝑇 × 𝐸 ) ↔ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) )
98 86 87 opth ⊢ ( ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ↔ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) )
99 98 rexbii ⊢ ( ∃ 𝑡 ∈ 𝐸 ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ↔ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) )
100 97 99 anbi12i ⊢ ( ( ⟨ 𝑖 , 𝑝 ⟩ ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) ↔ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) )
101 96 100 bitr4di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ↔ ( ⟨ 𝑖 , 𝑝 ⟩ ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) ) )
102 eqeq1 ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑝 ⟩ → ( 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ↔ ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) )
103 102 rexbidv ⊢ ( 𝑢 = ⟨ 𝑖 , 𝑝 ⟩ → ( ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ↔ ∃ 𝑡 ∈ 𝐸 ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) )
104 103 elrab ⊢ ( ⟨ 𝑖 , 𝑝 ⟩ ∈ { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } ↔ ( ⟨ 𝑖 , 𝑝 ⟩ ∈ ( 𝑇 × 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ⟨ 𝑖 , 𝑝 ⟩ = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ ) )
105 101 104 bitr4di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ↔ ⟨ 𝑖 , 𝑝 ⟩ ∈ { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } ) )
106 94 105 bitr2id ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ⟨ 𝑖 , 𝑝 ⟩ ∈ { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } ↔ ⟨ 𝑖 , 𝑝 ⟩ ∈ { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } ) )
107 84 85 106 eqrelrdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → { 𝑢 ∈ ( 𝑇 × 𝐸 ) ∣ ∃ 𝑡 ∈ 𝐸 𝑢 = ⟨ ( 𝑡 ‘ 𝑓 ) , ( 𝑡 ∘ 𝑠 ) ⟩ } = { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } )
108 80 107 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → { 𝑢 ∣ ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) } = { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } )
109 1 2 53 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑈 ∈ LMod )
110 1 9 11 2 15 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ 𝑉 )
111 110 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ 𝑉 )
112 13 54 15 16 18 lspsn ⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ 𝑉 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) = { 𝑢 ∣ ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) } )
113 109 111 112 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) = { 𝑢 ∣ ∃ 𝑡 ∈ ( Base ‘ 𝐹 ) 𝑢 = ( 𝑡 · ⟨ 𝑓 , 𝑠 ⟩ ) } )
114 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑠 ≠ 𝑂 )
115 5 1 9 11 12 2 13 14 tendoinvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ∧ ( 𝐽 ‘ 𝑠 ) ≠ 𝑂 ) )
116 115 simpld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) → ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 )
117 53 70 114 116 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 )
118 1 9 11 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 )
119 53 117 68 118 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 )
120 6 7 1 8 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) )
121 53 120 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) )
122 6 7 1 9 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) )
123 53 119 121 122 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) )
124 eqid ⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
125 6 7 1 124 3 dihvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) = ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) )
126 53 123 125 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐼 ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) = ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) )
127 6 7 1 8 9 11 124 20 dicval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) = { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } )
128 53 123 127 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) = { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } )
129 126 128 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐼 ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) = { ⟨ 𝑔 , 𝑟 ⟩ ∣ ( 𝑔 = ( 𝑟 ‘ 𝐺 ) ∧ 𝑟 ∈ 𝐸 ) } )
130 108 113 129 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) = ( 𝐼 ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) )
131 5 1 3 dihfn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn 𝐵 )
132 131 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝐼 Fn 𝐵 )
133 132 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝐼 Fn 𝐵 )
134 simplll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝐾 ∈ HL )
135 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
136 134 135 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝐾 ∈ OP )
137 5 1 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
138 137 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑊 ∈ 𝐵 )
139 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
140 5 139 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐵 )
141 136 138 140 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐵 )
142 8 141 eqeltrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → 𝑃 ∈ 𝐵 )
143 5 1 9 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐵 )
144 53 119 142 143 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐵 )
145 fnfvelrn ⊢ ( ( 𝐼 Fn 𝐵 ∧ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) ∈ ran 𝐼 )
146 133 144 145 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐼 ‘ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) ∈ ran 𝐼 )
147 130 146 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) ∈ ran 𝐼 )
148 52 147 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) ∈ ran 𝐼 )
149 148 ralrimivva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑓 ∈ 𝑇 ∀ 𝑠 ∈ 𝐸 ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) ∈ ran 𝐼 )
150 sneq ⊢ ( 𝑣 = ⟨ 𝑓 , 𝑠 ⟩ → { 𝑣 } = { ⟨ 𝑓 , 𝑠 ⟩ } )
151 150 fveq2d ⊢ ( 𝑣 = ⟨ 𝑓 , 𝑠 ⟩ → ( 𝑁 ‘ { 𝑣 } ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) )
152 151 eleq1d ⊢ ( 𝑣 = ⟨ 𝑓 , 𝑠 ⟩ → ( ( 𝑁 ‘ { 𝑣 } ) ∈ ran 𝐼 ↔ ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) ∈ ran 𝐼 ) )
153 152 ralxp ⊢ ( ∀ 𝑣 ∈ ( 𝑇 × 𝐸 ) ( 𝑁 ‘ { 𝑣 } ) ∈ ran 𝐼 ↔ ∀ 𝑓 ∈ 𝑇 ∀ 𝑠 ∈ 𝐸 ( 𝑁 ‘ { ⟨ 𝑓 , 𝑠 ⟩ } ) ∈ ran 𝐼 )
154 149 153 sylibr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑣 ∈ ( 𝑇 × 𝐸 ) ( 𝑁 ‘ { 𝑣 } ) ∈ ran 𝐼 )
155 154 r19.21bi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑁 ‘ { 𝑣 } ) ∈ ran 𝐼 )
156 30 155 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑣 } ) ∈ ran 𝐼 )
157 eleq1a ⊢ ( ( 𝑁 ‘ { 𝑣 } ) ∈ ran 𝐼 → ( 𝐷 = ( 𝑁 ‘ { 𝑣 } ) → 𝐷 ∈ ran 𝐼 ) )
158 156 157 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐷 = ( 𝑁 ‘ { 𝑣 } ) → 𝐷 ∈ ran 𝐼 ) )
159 158 rexlimdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) 𝐷 = ( 𝑁 ‘ { 𝑣 } ) → 𝐷 ∈ ran 𝐼 ) )
160 159 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝑉 ∖ { 0 } ) 𝐷 = ( 𝑁 ‘ { 𝑣 } ) → 𝐷 ∈ ran 𝐼 ) )
161 25 160 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝐴 ) → 𝐷 ∈ ran 𝐼 )