| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 2 |  | eqid 2737 | . . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 3 |  | dihatlat.a | . . . . 5
⊢ 𝐴 = (Atoms‘𝐾) | 
| 4 |  | dihatlat.h | . . . . 5
⊢ 𝐻 = (LHyp‘𝐾) | 
| 5 |  | eqid 2737 | . . . . 5
⊢
((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) | 
| 6 |  | eqid 2737 | . . . . 5
⊢ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) | 
| 7 |  | dihatlat.u | . . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | 
| 8 |  | dihatlat.i | . . . . 5
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) | 
| 9 |  | eqid 2737 | . . . . 5
⊢
(LSpan‘𝑈) =
(LSpan‘𝑈) | 
| 10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | dih1dimb2 41243 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄(le‘𝐾)𝑊)) → ∃𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉}))) | 
| 11 | 10 | anassrs 467 | . . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → ∃𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉}))) | 
| 12 |  | simp3rr 1248 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})) | 
| 13 |  | simp1l 1198 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 14 | 4, 7, 13 | dvhlmod 41112 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → 𝑈 ∈ LMod) | 
| 15 |  | simp3l 1202 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) | 
| 16 |  | eqid 2737 | . . . . . . . . 9
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) | 
| 17 | 1, 4, 5, 16, 6 | tendo0cl 40792 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) ∈ ((TEndo‘𝐾)‘𝑊)) | 
| 18 | 13, 17 | syl 17 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) ∈ ((TEndo‘𝐾)‘𝑊)) | 
| 19 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝑈) =
(Base‘𝑈) | 
| 20 | 4, 5, 16, 7, 19 | dvhelvbasei 41090 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) ∈ ((TEndo‘𝐾)‘𝑊))) → 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ∈
(Base‘𝑈)) | 
| 21 | 13, 15, 18, 20 | syl12anc 837 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) →
〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ∈
(Base‘𝑈)) | 
| 22 |  | simp3rl 1247 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → 𝑔 ≠ ( I ↾
(Base‘𝐾))) | 
| 23 | 22 | neneqd 2945 | . . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → ¬
𝑔 = ( I ↾
(Base‘𝐾))) | 
| 24 | 23 | intnanrd 489 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → ¬
(𝑔 = ( I ↾
(Base‘𝐾)) ∧
(𝑓 ∈
((LTrn‘𝐾)‘𝑊) ↦ ( I ↾
(Base‘𝐾))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))))) | 
| 25 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑔 ∈ V | 
| 26 |  | fvex 6919 | . . . . . . . . . . 11
⊢
((LTrn‘𝐾)‘𝑊) ∈ V | 
| 27 | 26 | mptex 7243 | . . . . . . . . . 10
⊢ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) ∈ V | 
| 28 | 25, 27 | opth 5481 | . . . . . . . . 9
⊢
(〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 = 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ↔ (𝑔 = ( I ↾ (Base‘𝐾)) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))))) | 
| 29 | 28 | necon3abii 2987 | . . . . . . . 8
⊢
(〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ≠ 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ↔ ¬ (𝑔 = ( I ↾ (Base‘𝐾)) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))))) | 
| 30 | 24, 29 | sylibr 234 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) →
〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ≠ 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉) | 
| 31 |  | eqid 2737 | . . . . . . . . 9
⊢
(0g‘𝑈) = (0g‘𝑈) | 
| 32 | 1, 4, 5, 7, 31, 6 | dvh0g 41113 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0g‘𝑈) = 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉) | 
| 33 | 13, 32 | syl 17 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) →
(0g‘𝑈) =
〈( I ↾ (Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉) | 
| 34 | 30, 33 | neeqtrrd 3015 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) →
〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ≠
(0g‘𝑈)) | 
| 35 |  | dihatlat.l | . . . . . . 7
⊢ 𝐿 = (LSAtoms‘𝑈) | 
| 36 | 19, 9, 31, 35 | lsatlspsn2 38993 | . . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ∈
(Base‘𝑈) ∧
〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ≠
(0g‘𝑈))
→ ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉}) ∈ 𝐿) | 
| 37 | 14, 21, 34, 36 | syl3anc 1373 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) →
((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉}) ∈ 𝐿) | 
| 38 | 12, 37 | eqeltrd 2841 | . . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊 ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → (𝐼‘𝑄) ∈ 𝐿) | 
| 39 | 38 | 3expa 1119 | . . 3
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑔 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉})))) → (𝐼‘𝑄) ∈ 𝐿) | 
| 40 | 11, 39 | rexlimddv 3161 | . 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → (𝐼‘𝑄) ∈ 𝐿) | 
| 41 |  | eqid 2737 | . . . . 5
⊢
((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊) | 
| 42 |  | eqid 2737 | . . . . 5
⊢
(℩𝑓
∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) = (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) | 
| 43 | 2, 3, 4, 41, 5, 8,
7, 9, 42 | dih1dimc 41244 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉})) | 
| 44 | 43 | anassrs 467 | . . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐼‘𝑄) = ((LSpan‘𝑈)‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉})) | 
| 45 |  | simpll 767 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 46 | 4, 7, 45 | dvhlmod 41112 | . . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 𝑈 ∈ LMod) | 
| 47 |  | eqid 2737 | . . . . . . . 8
⊢
(oc‘𝐾) =
(oc‘𝐾) | 
| 48 | 2, 47, 3, 4 | lhpocnel 40020 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) | 
| 49 | 48 | ad2antrr 726 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) | 
| 50 |  | simplr 769 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 𝑄 ∈ 𝐴) | 
| 51 |  | simpr 484 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ¬ 𝑄(le‘𝐾)𝑊) | 
| 52 | 2, 3, 4, 5, 42 | ltrniotacl 40581 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ ((LTrn‘𝐾)‘𝑊)) | 
| 53 | 45, 49, 50, 51, 52 | syl112anc 1376 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ ((LTrn‘𝐾)‘𝑊)) | 
| 54 | 4, 5, 16 | tendoidcl 40771 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊)) | 
| 55 | 54 | ad2antrr 726 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊)) | 
| 56 | 4, 5, 16, 7, 19 | dvhelvbasei 41090 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ ((LTrn‘𝐾)‘𝑊) ∧ ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊))) → 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ (Base‘𝑈)) | 
| 57 | 45, 53, 55, 56 | syl12anc 837 | . . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ (Base‘𝑈)) | 
| 58 | 1, 4, 5, 16, 6 | tendo1ne0 40830 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ≠ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))) | 
| 59 | 58 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ≠ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))) | 
| 60 | 59 | neneqd 2945 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ¬ ( I ↾
((LTrn‘𝐾)‘𝑊)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))) | 
| 61 | 60 | intnand 488 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ¬ ((℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) = ( I ↾ (Base‘𝐾)) ∧ ( I ↾
((LTrn‘𝐾)‘𝑊)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))))) | 
| 62 |  | riotaex 7392 | . . . . . . . 8
⊢
(℩𝑓
∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ V | 
| 63 |  | resiexg 7934 | . . . . . . . . 9
⊢
(((LTrn‘𝐾)‘𝑊) ∈ V → ( I ↾
((LTrn‘𝐾)‘𝑊)) ∈ V) | 
| 64 | 26, 63 | ax-mp 5 | . . . . . . . 8
⊢ ( I
↾ ((LTrn‘𝐾)‘𝑊)) ∈ V | 
| 65 | 62, 64 | opth 5481 | . . . . . . 7
⊢
(〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 = 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ↔
((℩𝑓 ∈
((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) = ( I ↾ (Base‘𝐾)) ∧ ( I ↾
((LTrn‘𝐾)‘𝑊)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))))) | 
| 66 | 65 | necon3abii 2987 | . . . . . 6
⊢
(〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ≠ 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉 ↔ ¬
((℩𝑓 ∈
((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) = ( I ↾ (Base‘𝐾)) ∧ ( I ↾
((LTrn‘𝐾)‘𝑊)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))))) | 
| 67 | 61, 66 | sylibr 234 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ≠ 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉) | 
| 68 | 32 | ad2antrr 726 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (0g‘𝑈) = 〈( I ↾
(Base‘𝐾)), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))〉) | 
| 69 | 67, 68 | neeqtrrd 3015 | . . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ≠ (0g‘𝑈)) | 
| 70 | 19, 9, 31, 35 | lsatlspsn2 38993 | . . . 4
⊢ ((𝑈 ∈ LMod ∧
〈(℩𝑓
∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ (Base‘𝑈) ∧
〈(℩𝑓
∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ≠ (0g‘𝑈)) → ((LSpan‘𝑈)‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉}) ∈ 𝐿) | 
| 71 | 46, 57, 69, 70 | syl3anc 1373 | . . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ((LSpan‘𝑈)‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉}) ∈ 𝐿) | 
| 72 | 44, 71 | eqeltrd 2841 | . 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐼‘𝑄) ∈ 𝐿) | 
| 73 | 40, 72 | pm2.61dan 813 | 1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → (𝐼‘𝑄) ∈ 𝐿) |