Step |
Hyp |
Ref |
Expression |
1 |
|
mapdval2.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
mapdval2.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
mapdval2.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑈 ) |
4 |
|
mapdval2.n |
⊢ 𝑁 = ( LSpan ‘ 𝑈 ) |
5 |
|
mapdval2.f |
⊢ 𝐹 = ( LFnl ‘ 𝑈 ) |
6 |
|
mapdval2.l |
⊢ 𝐿 = ( LKer ‘ 𝑈 ) |
7 |
|
mapdval2.o |
⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
|
mapdval2.m |
⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) |
9 |
|
mapdval2.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
10 |
|
mapdval2.t |
⊢ ( 𝜑 → 𝑇 ∈ 𝑆 ) |
11 |
|
mapdval2.c |
⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } |
12 |
1 2 3 5 6 7 8 9 10 11
|
mapdvalc |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 } ) |
13 |
1 2 9
|
dvhlmod |
⊢ ( 𝜑 → 𝑈 ∈ LMod ) |
14 |
13
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → 𝑈 ∈ LMod ) |
15 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) |
16 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
17 |
|
eqid |
⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 ) |
18 |
16 4 17
|
islsati |
⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
19 |
14 15 18
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
20 |
|
simprr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
21 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) |
22 |
20 21
|
eqsstrrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 ) |
23 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑈 ∈ LMod ) |
24 |
23
|
ad3antrrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑈 ∈ LMod ) |
25 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑇 ∈ 𝑆 ) |
26 |
25
|
ad3antrrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑇 ∈ 𝑆 ) |
27 |
|
simprl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) ) |
28 |
16 3 4 24 26 27
|
lspsnel5 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → ( 𝑣 ∈ 𝑇 ↔ ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 ) ) |
29 |
22 28
|
mpbird |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) → 𝑣 ∈ 𝑇 ) |
30 |
19 29 20
|
reximssdv |
⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
31 |
30
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) |
32 |
|
eqid |
⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 ) |
33 |
32 3
|
lss0cl |
⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → ( 0g ‘ 𝑈 ) ∈ 𝑇 ) |
34 |
13 10 33
|
syl2anc |
⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ 𝑇 ) |
35 |
34
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 0g ‘ 𝑈 ) ∈ 𝑇 ) |
36 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) |
37 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → 𝑈 ∈ LMod ) |
38 |
32 4
|
lspsn0 |
⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } ) |
39 |
37 38
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } ) |
40 |
36 39
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) |
41 |
|
sneq |
⊢ ( 𝑣 = ( 0g ‘ 𝑈 ) → { 𝑣 } = { ( 0g ‘ 𝑈 ) } ) |
42 |
41
|
fveq2d |
⊢ ( 𝑣 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑣 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) |
43 |
42
|
rspceeqv |
⊢ ( ( ( 0g ‘ 𝑈 ) ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
44 |
35 40 43
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
45 |
44
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
46 |
45
|
a1d |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) |
47 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
48 |
11
|
lcfl1lem |
⊢ ( 𝑓 ∈ 𝐶 ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ) |
49 |
48
|
simplbi |
⊢ ( 𝑓 ∈ 𝐶 → 𝑓 ∈ 𝐹 ) |
50 |
49
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → 𝑓 ∈ 𝐹 ) |
51 |
1 7 2 32 17 5 6 47 50
|
dochsat0 |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = { ( 0g ‘ 𝑈 ) } ) ) |
52 |
31 46 51
|
mpjaodan |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 → ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) |
53 |
|
simp3 |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) |
54 |
23
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → 𝑈 ∈ LMod ) |
55 |
25
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → 𝑇 ∈ 𝑆 ) |
56 |
|
simp2 |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → 𝑣 ∈ 𝑇 ) |
57 |
3 4 54 55 56
|
lspsnel5a |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑇 ) |
58 |
53 57
|
eqsstrd |
⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) ∧ 𝑣 ∈ 𝑇 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) |
59 |
58
|
rexlimdv3a |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) |
60 |
52 59
|
impbid |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ↔ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) ) ) |
61 |
60
|
rabbidva |
⊢ ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 } = { 𝑓 ∈ 𝐶 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } ) |
62 |
12 61
|
eqtrd |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐶 ∣ ∃ 𝑣 ∈ 𝑇 ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑣 } ) } ) |