Proof of Theorem mapdval2N
Step | Hyp | Ref
| Expression |
1 | | mapdval2.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | mapdval2.u |
. . 3
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | mapdval2.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑈) |
4 | | mapdval2.f |
. . 3
⊢ 𝐹 = (LFnl‘𝑈) |
5 | | mapdval2.l |
. . 3
⊢ 𝐿 = (LKer‘𝑈) |
6 | | mapdval2.o |
. . 3
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
7 | | mapdval2.m |
. . 3
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
8 | | mapdval2.k |
. . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
9 | | mapdval2.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
10 | | mapdval2.c |
. . 3
⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mapdvalc 35936 |
. 2
⊢ (𝜑 → (𝑀‘𝑇) = {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇}) |
12 | 1, 2, 8 | dvhlmod 35417 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ LMod) |
13 | 12 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) → 𝑈 ∈ LMod) |
14 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) → (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) |
15 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑈) =
(Base‘𝑈) |
16 | | mapdval2.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑈) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢
(LSAtoms‘𝑈) =
(LSAtoms‘𝑈) |
18 | 15, 16, 17 | islsati 33299 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) → ∃𝑣 ∈ (Base‘𝑈)(𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
19 | 13, 14, 18 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) → ∃𝑣 ∈ (Base‘𝑈)(𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
20 | | simprr 792 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
21 | | simplr 788 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) |
22 | 20, 21 | eqsstr3d 3603 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → (𝑁‘{𝑣}) ⊆ 𝑇) |
23 | 12 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑈 ∈ LMod) |
24 | 23 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → 𝑈 ∈ LMod) |
25 | 9 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑇 ∈ 𝑆) |
26 | 25 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → 𝑇 ∈ 𝑆) |
27 | | simprl 790 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → 𝑣 ∈ (Base‘𝑈)) |
28 | 15, 3, 16, 24, 26, 27 | lspsnel5 18816 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → (𝑣 ∈ 𝑇 ↔ (𝑁‘{𝑣}) ⊆ 𝑇)) |
29 | 22, 28 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → 𝑣 ∈ 𝑇) |
30 | 29, 20 | jca 553 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) ∧ (𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) → (𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) |
31 | 30 | ex 449 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) → ((𝑣 ∈ (Base‘𝑈) ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → (𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})))) |
32 | 31 | reximdv2 2997 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) → (∃𝑣 ∈ (Base‘𝑈)(𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}) → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) |
33 | 19, 32 | mpd 15 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
34 | 33 | ex 449 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈)) → ((𝑂‘(𝐿‘𝑓)) ⊆ 𝑇 → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) |
35 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑈) = (0g‘𝑈) |
36 | 35, 3 | lss0cl 18768 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑆) → (0g‘𝑈) ∈ 𝑇) |
37 | 12, 9, 36 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑈) ∈ 𝑇) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → (0g‘𝑈) ∈ 𝑇) |
39 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) |
40 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → 𝑈 ∈ LMod) |
41 | 35, 16 | lspsn0 18829 |
. . . . . . . . . 10
⊢ (𝑈 ∈ LMod → (𝑁‘{(0g‘𝑈)}) =
{(0g‘𝑈)}) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → (𝑁‘{(0g‘𝑈)}) =
{(0g‘𝑈)}) |
43 | 39, 42 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → (𝑂‘(𝐿‘𝑓)) = (𝑁‘{(0g‘𝑈)})) |
44 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑣 = (0g‘𝑈) → {𝑣} = {(0g‘𝑈)}) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑣 = (0g‘𝑈) → (𝑁‘{𝑣}) = (𝑁‘{(0g‘𝑈)})) |
46 | 45 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑣 = (0g‘𝑈) → ((𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}) ↔ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{(0g‘𝑈)}))) |
47 | 46 | rspcev 3282 |
. . . . . . . 8
⊢
(((0g‘𝑈) ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{(0g‘𝑈)})) → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
48 | 38, 43, 47 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
49 | 48 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
50 | 49 | a1d 25 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)}) → ((𝑂‘(𝐿‘𝑓)) ⊆ 𝑇 → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) |
51 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
52 | 10 | lcfl1lem 35798 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐶 ↔ (𝑓 ∈ 𝐹 ∧ (𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓))) |
53 | 52 | simplbi 475 |
. . . . . . 7
⊢ (𝑓 ∈ 𝐶 → 𝑓 ∈ 𝐹) |
54 | 53 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ 𝐹) |
55 | 1, 6, 2, 35, 17, 4, 5, 51, 54 | dochsat0 35764 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → ((𝑂‘(𝐿‘𝑓)) ∈ (LSAtoms‘𝑈) ∨ (𝑂‘(𝐿‘𝑓)) = {(0g‘𝑈)})) |
56 | 34, 50, 55 | mpjaodan 823 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → ((𝑂‘(𝐿‘𝑓)) ⊆ 𝑇 → ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) |
57 | | simp3 1056 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ 𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) |
58 | 23 | 3ad2ant1 1075 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ 𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → 𝑈 ∈ LMod) |
59 | 25 | 3ad2ant1 1075 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ 𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → 𝑇 ∈ 𝑆) |
60 | | simp2 1055 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ 𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → 𝑣 ∈ 𝑇) |
61 | 3, 16, 58, 59, 60 | lspsnel5a 18817 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ 𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → (𝑁‘{𝑣}) ⊆ 𝑇) |
62 | 57, 61 | eqsstrd 3602 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐶) ∧ 𝑣 ∈ 𝑇 ∧ (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})) → (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇) |
63 | 62 | rexlimdv3a 3015 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → (∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}) → (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇)) |
64 | 56, 63 | impbid 201 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐶) → ((𝑂‘(𝐿‘𝑓)) ⊆ 𝑇 ↔ ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣}))) |
65 | 64 | rabbidva 3163 |
. 2
⊢ (𝜑 → {𝑓 ∈ 𝐶 ∣ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑇} = {𝑓 ∈ 𝐶 ∣ ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})}) |
66 | 11, 65 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑀‘𝑇) = {𝑓 ∈ 𝐶 ∣ ∃𝑣 ∈ 𝑇 (𝑂‘(𝐿‘𝑓)) = (𝑁‘{𝑣})}) |