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

Metamath Proof Explorer

Theorem dihatlat

Description: The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014)

Ref Expression
Hypotheses dihatlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihatlat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihatlat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihatlat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihatlat.l ⊢ 𝐿 = ( LSAtoms ‘ 𝑈 )
Assertion dihatlat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → ( 𝐼 ‘ 𝑄 ) ∈ 𝐿 )

Proof

Step Hyp Ref Expression
1 dihatlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 dihatlat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihatlat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dihatlat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 dihatlat.l ⊢ 𝐿 = ( LSAtoms ‘ 𝑈 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
10 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
11 6 7 1 2 8 9 3 4 10 dih1dimb2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ) → ∃ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) )
12 11 anassrs ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ∃ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) )
13 simp3rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) )
14 simp1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15 2 3 14 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → 𝑈 ∈ LMod )
16 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
17 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
18 6 2 8 17 9 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
19 14 18 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
20 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
21 2 8 17 3 20 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ∈ ( Base ‘ 𝑈 ) )
22 14 16 19 21 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ∈ ( Base ‘ 𝑈 ) )
23 simp3rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) )
24 23 neneqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ¬ 𝑔 = ( I ↾ ( Base ‘ 𝐾 ) ) )
25 24 intnanrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ¬ ( 𝑔 = ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) )
26 vex ⊢ 𝑔 ∈ V
27 fvex ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
28 27 mptex ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ V
29 26 28 opth ⊢ ( ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ↔ ( 𝑔 = ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) )
30 29 necon3abii ⊢ ( ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ≠ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ↔ ¬ ( 𝑔 = ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) )
31 25 30 sylibr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ≠ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ )
32 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
33 6 2 8 3 32 9 dvh0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝑈 ) = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ )
34 14 33 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( 0g ‘ 𝑈 ) = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ )
35 31 34 neeqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ≠ ( 0g ‘ 𝑈 ) )
36 20 10 32 5 lsatlspsn2 ⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ∈ ( Base ‘ 𝑈 ) ∧ ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ≠ ( 0g ‘ 𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ∈ 𝐿 )
37 15 22 35 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ∈ 𝐿 )
38 13 37 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( 𝐼 ‘ 𝑄 ) ∈ 𝐿 )
39 38 3expa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑔 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } ) ) ) ) → ( 𝐼 ‘ 𝑄 ) ∈ 𝐿 )
40 12 39 rexlimddv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑄 ) ∈ 𝐿 )
41 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
42 eqid ⊢ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 )
43 7 1 2 41 8 4 3 10 42 dih1dimc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) )
44 43 anassrs ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑄 ) = ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) )
45 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
46 2 3 45 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → 𝑈 ∈ LMod )
47 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
48 7 47 1 2 lhpocnel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) )
49 48 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) )
50 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → 𝑄 ∈ 𝐴 )
51 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 )
52 7 1 2 8 42 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
53 45 49 50 51 52 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
54 2 8 17 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
55 54 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
56 2 8 17 3 20 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( Base ‘ 𝑈 ) )
57 45 53 55 56 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( Base ‘ 𝑈 ) )
58 6 2 8 17 9 tendo1ne0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ≠ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
59 58 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ≠ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
60 59 neneqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ¬ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
61 60 intnand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ¬ ( ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) )
62 riotaex ⊢ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ V
63 resiexg ⊢ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ V )
64 27 63 ax-mp ⊢ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ V
65 62 64 opth ⊢ ( ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ↔ ( ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) )
66 65 necon3abii ⊢ ( ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ≠ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ ↔ ¬ ( ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) )
67 61 66 sylibr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ≠ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ )
68 33 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 0g ‘ 𝑈 ) = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ )
69 67 68 neeqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ≠ ( 0g ‘ 𝑈 ) )
70 20 10 32 5 lsatlspsn2 ⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( Base ‘ 𝑈 ) ∧ ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ≠ ( 0g ‘ 𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∈ 𝐿 )
71 46 57 69 70 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∈ 𝐿 )
72 44 71 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑄 ) ∈ 𝐿 )
73 40 72 pm2.61dan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → ( 𝐼 ‘ 𝑄 ) ∈ 𝐿 )