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 |
⊢ ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 ) |