Step | Hyp | Ref
| Expression |
1 | | mapd1o.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑈) |
2 | | fvex 6201 |
. . . . . 6
⊢
(LFnl‘𝑈)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. . . . 5
⊢ 𝐹 ∈ V |
4 | 3 | rabex 4813 |
. . . 4
⊢ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)} ∈ V |
5 | | eqid 2622 |
. . . 4
⊢ (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) = (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) |
6 | 4, 5 | fnmpti 6022 |
. . 3
⊢ (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) Fn 𝑆 |
7 | | mapd1o.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | | mapd1o.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
9 | | mapd1o.u |
. . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
10 | | mapd1o.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑈) |
11 | | mapd1o.l |
. . . . . 6
⊢ 𝐿 = (LKer‘𝑈) |
12 | | mapd1o.o |
. . . . . 6
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
13 | | mapd1o.m |
. . . . . 6
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
14 | 8, 9, 10, 1, 11, 12, 13 | mapdfval 36916 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)})) |
15 | 7, 14 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)})) |
16 | 15 | fneq1d 5981 |
. . 3
⊢ (𝜑 → (𝑀 Fn 𝑆 ↔ (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) Fn 𝑆)) |
17 | 6, 16 | mpbiri 248 |
. 2
⊢ (𝜑 → 𝑀 Fn 𝑆) |
18 | 3 | rabex 4813 |
. . . . . . 7
⊢ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)} ∈ V |
19 | | eqid 2622 |
. . . . . . 7
⊢ (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) = (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) |
20 | 18, 19 | fnmpti 6022 |
. . . . . 6
⊢ (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) Fn 𝑆 |
21 | 8, 9, 10, 1, 11, 12, 13 | mapdfval 36916 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)})) |
22 | 7, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)})) |
23 | 22 | fneq1d 5981 |
. . . . . 6
⊢ (𝜑 → (𝑀 Fn 𝑆 ↔ (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) Fn 𝑆)) |
24 | 20, 23 | mpbiri 248 |
. . . . 5
⊢ (𝜑 → 𝑀 Fn 𝑆) |
25 | | fvelrnb 6243 |
. . . . 5
⊢ (𝑀 Fn 𝑆 → (𝑡 ∈ ran 𝑀 ↔ ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡)) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ ran 𝑀 ↔ ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡)) |
27 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
28 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → 𝑐 ∈ 𝑆) |
29 | 8, 9, 10, 1, 11, 12, 13, 27, 28 | mapdval 36917 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → (𝑀‘𝑐) = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)}) |
30 | | mapd1o.d |
. . . . . . . . . 10
⊢ 𝐷 = (LDual‘𝑈) |
31 | | mapd1o.t |
. . . . . . . . . 10
⊢ 𝑇 = (LSubSp‘𝐷) |
32 | | mapd1o.c |
. . . . . . . . . 10
⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} |
33 | | eqid 2622 |
. . . . . . . . . 10
⊢ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} |
34 | 8, 12, 9, 10, 1, 11, 30, 31, 32, 33, 27, 28 | lclkrs2 36829 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶)) |
35 | | elin 3796 |
. . . . . . . . . 10
⊢ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ (𝑇 ∩ 𝒫 𝐶) ↔ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝒫 𝐶)) |
36 | 3 | rabex 4813 |
. . . . . . . . . . . 12
⊢ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ V |
37 | 36 | elpw 4164 |
. . . . . . . . . . 11
⊢ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝒫 𝐶 ↔ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶) |
38 | 37 | anbi2i 730 |
. . . . . . . . . 10
⊢ (({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝒫 𝐶) ↔ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶)) |
39 | 35, 38 | bitr2i 265 |
. . . . . . . . 9
⊢ (({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶) ↔ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ (𝑇 ∩ 𝒫 𝐶)) |
40 | 34, 39 | sylib 208 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ (𝑇 ∩ 𝒫 𝐶)) |
41 | 29, 40 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → (𝑀‘𝑐) ∈ (𝑇 ∩ 𝒫 𝐶)) |
42 | | eleq1 2689 |
. . . . . . 7
⊢ ((𝑀‘𝑐) = 𝑡 → ((𝑀‘𝑐) ∈ (𝑇 ∩ 𝒫 𝐶) ↔ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
43 | 41, 42 | syl5ibcom 235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → ((𝑀‘𝑐) = 𝑡 → 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
44 | 43 | rexlimdva 3031 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡 → 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
45 | | eqid 2622 |
. . . . . . . 8
⊢ ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) = ∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) |
46 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
47 | | inss1 3833 |
. . . . . . . . . 10
⊢ (𝑇 ∩ 𝒫 𝐶) ⊆ 𝑇 |
48 | 47 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → 𝑡 ∈ 𝑇) |
49 | 48 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → 𝑡 ∈ 𝑇) |
50 | | inss2 3834 |
. . . . . . . . . . 11
⊢ (𝑇 ∩ 𝒫 𝐶) ⊆ 𝒫 𝐶 |
51 | 50 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → 𝑡 ∈ 𝒫 𝐶) |
52 | 51 | elpwid 4170 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → 𝑡 ⊆ 𝐶) |
53 | 52 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → 𝑡 ⊆ 𝐶) |
54 | 8, 12, 9, 10, 1, 11, 30, 31, 32, 45, 46, 49, 53 | lcfr 36874 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) ∈ 𝑆) |
55 | 8, 12, 13, 9, 10, 1, 11, 30, 31, 32, 46, 49, 53, 45 | mapdrval 36936 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓))) = 𝑡) |
56 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑐 = ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) → (𝑀‘𝑐) = (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)))) |
57 | 56 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑐 = ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) → ((𝑀‘𝑐) = 𝑡 ↔ (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓))) = 𝑡)) |
58 | 57 | rspcev 3309 |
. . . . . . 7
⊢
((∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) ∈ 𝑆 ∧ (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓))) = 𝑡) → ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡) |
59 | 54, 55, 58 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡) |
60 | 59 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡)) |
61 | 44, 60 | impbid 202 |
. . . 4
⊢ (𝜑 → (∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡 ↔ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
62 | 26, 61 | bitrd 268 |
. . 3
⊢ (𝜑 → (𝑡 ∈ ran 𝑀 ↔ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
63 | 62 | eqrdv 2620 |
. 2
⊢ (𝜑 → ran 𝑀 = (𝑇 ∩ 𝒫 𝐶)) |
64 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
65 | | simprl 794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝑡 ∈ 𝑆) |
66 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆) |
67 | 8, 9, 10, 13, 64, 65, 66 | mapd11 36928 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑀‘𝑡) = (𝑀‘𝑢) ↔ 𝑡 = 𝑢)) |
68 | 67 | biimpd 219 |
. . 3
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑀‘𝑡) = (𝑀‘𝑢) → 𝑡 = 𝑢)) |
69 | 68 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑀‘𝑡) = (𝑀‘𝑢) → 𝑡 = 𝑢)) |
70 | | dff1o6 6531 |
. 2
⊢ (𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶) ↔ (𝑀 Fn 𝑆 ∧ ran 𝑀 = (𝑇 ∩ 𝒫 𝐶) ∧ ∀𝑡 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑀‘𝑡) = (𝑀‘𝑢) → 𝑡 = 𝑢))) |
71 | 17, 63, 69, 70 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶)) |