Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . 3
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑀 ∈ V) |
3 | | lcoop.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
4 | 3 | pweqi 4112 |
. . . . 5
⊢ 𝒫
𝐵 = 𝒫
(Base‘𝑀) |
5 | 4 | eleq2i 2680 |
. . . 4
⊢ (𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 (Base‘𝑀)) |
6 | 5 | biimpi 205 |
. . 3
⊢ (𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
7 | 6 | adantl 481 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
8 | | fvex 6113 |
. . . 4
⊢
(Base‘𝑀)
∈ V |
9 | 3, 8 | eqeltri 2684 |
. . 3
⊢ 𝐵 ∈ V |
10 | | rabexg 4739 |
. . 3
⊢ (𝐵 ∈ V → {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))} ∈ V) |
11 | 9, 10 | mp1i 13 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))} ∈ V) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
13 | 12, 3 | syl6eqr 2662 |
. . . . 5
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = 𝐵) |
14 | 13 | adantr 480 |
. . . 4
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (Base‘𝑚) = 𝐵) |
15 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀)) |
16 | 15 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) |
18 | | lcoop.r |
. . . . . . . 8
⊢ 𝑅 = (Base‘𝑆) |
19 | | lcoop.s |
. . . . . . . . 9
⊢ 𝑆 = (Scalar‘𝑀) |
20 | 19 | fveq2i 6106 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
21 | 18, 20 | eqtri 2632 |
. . . . . . 7
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
22 | 17, 21 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (Base‘(Scalar‘𝑚)) = 𝑅) |
23 | | simpr 476 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉) |
24 | 22, 23 | oveq12d 6567 |
. . . . 5
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣) = (𝑅 ↑𝑚 𝑉)) |
25 | 15 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 →
(0g‘(Scalar‘𝑚)) = (0g‘(Scalar‘𝑀))) |
26 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → 𝑆 = (Scalar‘𝑀)) |
27 | 26 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (Scalar‘𝑀) = 𝑆) |
28 | 27 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 →
(0g‘(Scalar‘𝑀)) = (0g‘𝑆)) |
29 | 25, 28 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 →
(0g‘(Scalar‘𝑚)) = (0g‘𝑆)) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) →
(0g‘(Scalar‘𝑚)) = (0g‘𝑆)) |
31 | 30 | breq2d 4595 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (𝑠 finSupp
(0g‘(Scalar‘𝑚)) ↔ 𝑠 finSupp (0g‘𝑆))) |
32 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → ( linC ‘𝑚) = ( linC ‘𝑀)) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → ( linC ‘𝑚) = ( linC ‘𝑀)) |
34 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → 𝑠 = 𝑠) |
35 | 33, 34, 23 | oveq123d 6570 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (𝑠( linC ‘𝑚)𝑣) = (𝑠( linC ‘𝑀)𝑉)) |
36 | 35 | eqeq2d 2620 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (𝑐 = (𝑠( linC ‘𝑚)𝑣) ↔ 𝑐 = (𝑠( linC ‘𝑀)𝑉))) |
37 | 31, 36 | anbi12d 743 |
. . . . 5
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → ((𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣)) ↔ (𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉)))) |
38 | 24, 37 | rexeqbidv 3130 |
. . . 4
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣)(𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣)) ↔ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉)))) |
39 | 14, 38 | rabeqbidv 3168 |
. . 3
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣)(𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))} = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) |
40 | 12 | pweqd 4113 |
. . 3
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) |
41 | | df-lco 41990 |
. . 3
⊢ LinCo =
(𝑚 ∈ V, 𝑣 ∈ 𝒫
(Base‘𝑚) ↦
{𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣)(𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}) |
42 | 39, 40, 41 | ovmpt2x 6687 |
. 2
⊢ ((𝑀 ∈ V ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))} ∈ V) → (𝑀 LinCo 𝑉) = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) |
43 | 2, 7, 11, 42 | syl3anc 1318 |
1
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) |