| Step | Hyp | Ref
| Expression |
| 1 | | mapd1o.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑈) |
| 2 | 1 | fvexi 6920 |
. . . . 5
⊢ 𝐹 ∈ V |
| 3 | 2 | rabex 5339 |
. . . 4
⊢ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)} ∈ V |
| 4 | | eqid 2737 |
. . . 4
⊢ (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) = (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) |
| 5 | 3, 4 | fnmpti 6711 |
. . 3
⊢ (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) Fn 𝑆 |
| 6 | | mapd1o.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 7 | | mapd1o.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
| 8 | | mapd1o.u |
. . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 9 | | mapd1o.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑈) |
| 10 | | mapd1o.l |
. . . . . 6
⊢ 𝐿 = (LKer‘𝑈) |
| 11 | | mapd1o.o |
. . . . . 6
⊢ 𝑂 = ((ocH‘𝐾)‘𝑊) |
| 12 | | mapd1o.m |
. . . . . 6
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
| 13 | 7, 8, 9, 1, 10, 11, 12 | mapdfval 41629 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)})) |
| 14 | 6, 13 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)})) |
| 15 | 14 | fneq1d 6661 |
. . 3
⊢ (𝜑 → (𝑀 Fn 𝑆 ↔ (𝑡 ∈ 𝑆 ↦ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑡)}) Fn 𝑆)) |
| 16 | 5, 15 | mpbiri 258 |
. 2
⊢ (𝜑 → 𝑀 Fn 𝑆) |
| 17 | 2 | rabex 5339 |
. . . . . . 7
⊢ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)} ∈ V |
| 18 | | eqid 2737 |
. . . . . . 7
⊢ (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) = (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) |
| 19 | 17, 18 | fnmpti 6711 |
. . . . . 6
⊢ (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) Fn 𝑆 |
| 20 | 7, 8, 9, 1, 10, 11, 12 | mapdfval 41629 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)})) |
| 21 | 6, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)})) |
| 22 | 21 | fneq1d 6661 |
. . . . . 6
⊢ (𝜑 → (𝑀 Fn 𝑆 ↔ (𝑡 ∈ 𝑆 ↦ {𝑔 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔) ∧ (𝑂‘(𝐿‘𝑔)) ⊆ 𝑡)}) Fn 𝑆)) |
| 23 | 19, 22 | mpbiri 258 |
. . . . 5
⊢ (𝜑 → 𝑀 Fn 𝑆) |
| 24 | | fvelrnb 6969 |
. . . . 5
⊢ (𝑀 Fn 𝑆 → (𝑡 ∈ ran 𝑀 ↔ ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡)) |
| 25 | 23, 24 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ ran 𝑀 ↔ ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡)) |
| 26 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 27 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → 𝑐 ∈ 𝑆) |
| 28 | 7, 8, 9, 1, 10, 11, 12, 26, 27 | mapdval 41630 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → (𝑀‘𝑐) = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)}) |
| 29 | | mapd1o.d |
. . . . . . . . . 10
⊢ 𝐷 = (LDual‘𝑈) |
| 30 | | mapd1o.t |
. . . . . . . . . 10
⊢ 𝑇 = (LSubSp‘𝐷) |
| 31 | | mapd1o.c |
. . . . . . . . . 10
⊢ 𝐶 = {𝑔 ∈ 𝐹 ∣ (𝑂‘(𝑂‘(𝐿‘𝑔))) = (𝐿‘𝑔)} |
| 32 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} = {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} |
| 33 | 7, 11, 8, 9, 1, 10,
29, 30, 31, 32, 26, 27 | lclkrs2 41542 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶)) |
| 34 | | elin 3967 |
. . . . . . . . . 10
⊢ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ (𝑇 ∩ 𝒫 𝐶) ↔ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝒫 𝐶)) |
| 35 | 2 | rabex 5339 |
. . . . . . . . . . . 12
⊢ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ V |
| 36 | 35 | elpw 4604 |
. . . . . . . . . . 11
⊢ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝒫 𝐶 ↔ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶) |
| 37 | 36 | anbi2i 623 |
. . . . . . . . . 10
⊢ (({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝒫 𝐶) ↔ ({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶)) |
| 38 | 34, 37 | bitr2i 276 |
. . . . . . . . 9
⊢ (({𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ 𝑇 ∧ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ⊆ 𝐶) ↔ {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ (𝑇 ∩ 𝒫 𝐶)) |
| 39 | 33, 38 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → {𝑓 ∈ 𝐹 ∣ ((𝑂‘(𝑂‘(𝐿‘𝑓))) = (𝐿‘𝑓) ∧ (𝑂‘(𝐿‘𝑓)) ⊆ 𝑐)} ∈ (𝑇 ∩ 𝒫 𝐶)) |
| 40 | 28, 39 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → (𝑀‘𝑐) ∈ (𝑇 ∩ 𝒫 𝐶)) |
| 41 | | eleq1 2829 |
. . . . . . 7
⊢ ((𝑀‘𝑐) = 𝑡 → ((𝑀‘𝑐) ∈ (𝑇 ∩ 𝒫 𝐶) ↔ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
| 42 | 40, 41 | syl5ibcom 245 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑆) → ((𝑀‘𝑐) = 𝑡 → 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
| 43 | 42 | rexlimdva 3155 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡 → 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
| 44 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) = ∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) |
| 45 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 46 | | inss1 4237 |
. . . . . . . . . 10
⊢ (𝑇 ∩ 𝒫 𝐶) ⊆ 𝑇 |
| 47 | 46 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → 𝑡 ∈ 𝑇) |
| 48 | 47 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → 𝑡 ∈ 𝑇) |
| 49 | | inss2 4238 |
. . . . . . . . . . 11
⊢ (𝑇 ∩ 𝒫 𝐶) ⊆ 𝒫 𝐶 |
| 50 | 49 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → 𝑡 ∈ 𝒫 𝐶) |
| 51 | 50 | elpwid 4609 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → 𝑡 ⊆ 𝐶) |
| 52 | 51 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → 𝑡 ⊆ 𝐶) |
| 53 | 7, 11, 8, 9, 1, 10,
29, 30, 31, 44, 45, 48, 52 | lcfr 41587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) ∈ 𝑆) |
| 54 | 7, 11, 12, 8, 9, 1,
10, 29, 30, 31, 45, 48, 52, 44 | mapdrval 41649 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓))) = 𝑡) |
| 55 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑐 = ∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) → ((𝑀‘𝑐) = 𝑡 ↔ (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓))) = 𝑡)) |
| 56 | 55 | rspcev 3622 |
. . . . . . 7
⊢
((∪ 𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓)) ∈ 𝑆 ∧ (𝑀‘∪
𝑓 ∈ 𝑡 (𝑂‘(𝐿‘𝑓))) = 𝑡) → ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡) |
| 57 | 53, 54, 56 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶)) → ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡) |
| 58 | 57 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝑇 ∩ 𝒫 𝐶) → ∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡)) |
| 59 | 43, 58 | impbid 212 |
. . . 4
⊢ (𝜑 → (∃𝑐 ∈ 𝑆 (𝑀‘𝑐) = 𝑡 ↔ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
| 60 | 25, 59 | bitrd 279 |
. . 3
⊢ (𝜑 → (𝑡 ∈ ran 𝑀 ↔ 𝑡 ∈ (𝑇 ∩ 𝒫 𝐶))) |
| 61 | 60 | eqrdv 2735 |
. 2
⊢ (𝜑 → ran 𝑀 = (𝑇 ∩ 𝒫 𝐶)) |
| 62 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 63 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝑡 ∈ 𝑆) |
| 64 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆) |
| 65 | 7, 8, 9, 12, 62, 63, 64 | mapd11 41641 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑀‘𝑡) = (𝑀‘𝑢) ↔ 𝑡 = 𝑢)) |
| 66 | 65 | biimpd 229 |
. . 3
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑀‘𝑡) = (𝑀‘𝑢) → 𝑡 = 𝑢)) |
| 67 | 66 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑀‘𝑡) = (𝑀‘𝑢) → 𝑡 = 𝑢)) |
| 68 | | dff1o6 7295 |
. 2
⊢ (𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶) ↔ (𝑀 Fn 𝑆 ∧ ran 𝑀 = (𝑇 ∩ 𝒫 𝐶) ∧ ∀𝑡 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑀‘𝑡) = (𝑀‘𝑢) → 𝑡 = 𝑢))) |
| 69 | 16, 61, 67, 68 | syl3anbrc 1344 |
1
⊢ (𝜑 → 𝑀:𝑆–1-1-onto→(𝑇 ∩ 𝒫 𝐶)) |