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 lspsnel5 ( ( ( ( 𝜑𝑓𝐶 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 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 lspsnel5a ( ( ( ( ( ( 𝜑𝑓𝐶 ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 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 ( 𝜑 → { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 )