Metamath Proof Explorer

Theorem mapdrvallem2

Description: Lemma for mapdrval . TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015)

Ref Expression
Hypotheses mapdrval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdrval.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdrval.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdrval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdrval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdrval.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapdrval.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapdrval.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
mapdrval.t ⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
mapdrval.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
mapdrval.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdrval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
mapdrval.e ⊢ ( 𝜑 → 𝑅 ⊆ 𝐶 )
mapdrval.q ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) )
mapdrval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdrvallem2.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
mapdrvallem2.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdrvallem2.z ⊢ 0 = ( 0g ‘ 𝑈 )
mapdrvallem2.y ⊢ 𝑌 = ( 0g ‘ 𝐷 )
Assertion mapdrvallem2 ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 )

Proof

Step Hyp Ref Expression
1 mapdrval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdrval.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdrval.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4 mapdrval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 mapdrval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6 mapdrval.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 mapdrval.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 mapdrval.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
9 mapdrval.t ⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
10 mapdrval.c ⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
11 mapdrval.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 mapdrval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
13 mapdrval.e ⊢ ( 𝜑 → 𝑅 ⊆ 𝐶 )
14 mapdrval.q ⊢ 𝑄 = ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) )
15 mapdrval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
16 mapdrvallem2.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
17 mapdrvallem2.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
18 mapdrvallem2.z ⊢ 0 = ( 0g ‘ 𝑈 )
19 mapdrvallem2.y ⊢ 𝑌 = ( 0g ‘ 𝐷 )
20 eleq1 ⊢ ( 𝑓 = 𝑌 → ( 𝑓 ∈ 𝑅 ↔ 𝑌 ∈ 𝑅 ) )
21 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ 𝐶 )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ≠ 𝑌 )
25 eldifsn ⊢ ( 𝑓 ∈ ( 𝐶 ∖ { 𝑌 } ) ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 ≠ 𝑌 ) )
26 23 24 25 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ ( 𝐶 ∖ { 𝑌 } ) )
27 1 2 4 15 17 18 6 7 8 19 10 22 26 lcfl8b ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) )
28 simp1l3 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 )
29 eqimss2 ⊢ ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
30 29 3ad2ant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
31 1 4 11 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
32 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑈 ∈ LMod )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑈 ∈ LMod )
34 33 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑈 ∈ LMod )
35 22 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
36 10 lcfl1lem ⊢ ( 𝑓 ∈ 𝐶 ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) )
37 36 simplbi ⊢ ( 𝑓 ∈ 𝐶 → 𝑓 ∈ 𝐹 )
38 37 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑓 ∈ 𝐹 )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ 𝐹 )
40 39 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑓 ∈ 𝐹 )
41 15 6 7 34 40 lkrssv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 )
42 1 4 15 5 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝑆 )
43 35 41 42 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝑆 )
44 eldifi ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) → 𝑥 ∈ 𝑉 )
45 44 3ad2ant2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑉 )
46 15 5 17 34 43 45 ellspsn5b ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
47 30 46 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
48 28 47 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑄 )
49 48 14 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
50 eliun ⊢ ( 𝑥 ∈ ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ↔ ∃ ℎ ∈ 𝑅 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
51 49 50 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ∃ ℎ ∈ 𝑅 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
52 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
53 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
54 eqid ⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
55 1 4 11 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
56 55 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑈 ∈ LVec )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑈 ∈ LVec )
58 57 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑈 ∈ LVec )
59 58 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑈 ∈ LVec )
60 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝑅 )
61 simp1l1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝜑 )
62 61 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → 𝜑 )
63 62 13 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → 𝑅 ⊆ 𝐶 )
64 63 sseld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ( ℎ ∈ 𝑅 → ℎ ∈ 𝐶 ) )
65 10 lcfl1lem ⊢ ( ℎ ∈ 𝐶 ↔ ( ℎ ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) = ( 𝐿 ‘ ℎ ) ) )
66 65 simplbi ⊢ ( ℎ ∈ 𝐶 → ℎ ∈ 𝐹 )
67 64 66 syl6 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ( ℎ ∈ 𝑅 → ℎ ∈ 𝐹 ) )
68 60 67 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝐹 )
69 68 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ℎ ∈ 𝐹 )
70 40 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑓 ∈ 𝐹 )
71 simpll3 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) )
72 34 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑈 ∈ LMod )
73 35 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
74 15 6 7 72 69 lkrssv ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ ℎ ) ⊆ 𝑉 )
75 1 4 15 5 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ ℎ ) ⊆ 𝑉 ) → ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ∈ 𝑆 )
76 73 74 75 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ∈ 𝑆 )
77 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
78 5 17 72 76 77 ellspsn5 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
79 simpll2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
80 15 17 18 16 72 79 lsatlspsn ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ∈ 𝐴 )
81 1 2 4 18 16 6 7 73 69 dochsat0 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ∈ 𝐴 ∨ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) = { 0 } ) )
82 18 16 59 80 81 lsatcmp2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ↔ ( 𝑁 ‘ { 𝑥 } ) = ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) )
83 78 82 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
84 71 83 eqtr2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
85 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
86 61 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑅 ⊆ 𝐶 )
87 86 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝐶 )
88 87 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ℎ ∈ 𝐶 )
89 1 85 2 4 6 7 10 73 69 lcfl5 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ℎ ∈ 𝐶 ↔ ( 𝐿 ‘ ℎ ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
90 88 89 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ ℎ ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
91 simp1l2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑓 ∈ 𝐶 )
92 91 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑓 ∈ 𝐶 )
93 1 85 2 4 6 7 10 73 70 lcfl5 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑓 ∈ 𝐶 ↔ ( 𝐿 ‘ 𝑓 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
94 92 93 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ 𝑓 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
95 1 85 2 73 90 94 doch11 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ( 𝐿 ‘ ℎ ) = ( 𝐿 ‘ 𝑓 ) ) )
96 84 95 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ ℎ ) = ( 𝐿 ‘ 𝑓 ) )
97 52 53 6 7 8 54 59 69 70 96 eqlkr4 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) )
98 97 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ( 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ) )
99 98 reximdva ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( ∃ ℎ ∈ 𝑅 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) → ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ) )
100 51 99 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) )
101 eleq1 ⊢ ( 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
102 101 reximi ⊢ ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
103 102 reximi ⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
104 rexcom ⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ∈ 𝑅 ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
105 df-rex ⊢ ( ∃ ℎ ∈ 𝑅 ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
106 105 rexbii ⊢ ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ∈ 𝑅 ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
107 104 106 bitri ⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
108 103 107 sylib ⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
109 100 108 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
110 33 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑈 ∈ LMod )
111 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑅 ∈ 𝑇 )
112 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑅 ∈ 𝑇 )
113 112 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑅 ∈ 𝑇 )
114 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
115 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → ℎ ∈ 𝑅 )
116 52 53 8 54 9 110 113 114 115 ldualssvscl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 )
117 biimpr ⊢ ( ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 → 𝑓 ∈ 𝑅 ) )
118 117 ad2antll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 → 𝑓 ∈ 𝑅 ) )
119 116 118 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑓 ∈ 𝑅 )
120 119 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
121 120 exlimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
122 121 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
123 122 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
124 109 123 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑓 ∈ 𝑅 )
125 124 rexlimdv3a ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) → 𝑓 ∈ 𝑅 ) )
126 27 125 mpd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ 𝑅 )
127 8 31 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
128 127 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝐷 ∈ LMod )
129 19 9 lss0cl ⊢ ( ( 𝐷 ∈ LMod ∧ 𝑅 ∈ 𝑇 ) → 𝑌 ∈ 𝑅 )
130 128 111 129 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑌 ∈ 𝑅 )
131 20 126 130 pm2.61ne ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑓 ∈ 𝑅 )
132 131 rabssdv ⊢ ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 )