| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3500 | . . 3
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) | 
| 2 | 1 | adantr 480 | . 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑀 ∈ V) | 
| 3 |  | lcoop.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑀) | 
| 4 | 3 | pweqi 4615 | . . . . 5
⊢ 𝒫
𝐵 = 𝒫
(Base‘𝑀) | 
| 5 | 4 | eleq2i 2832 | . . . 4
⊢ (𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 6 | 5 | biimpi 216 | . . 3
⊢ (𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 7 | 6 | adantl 481 | . 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 8 | 3 | fvexi 6919 | . . 3
⊢ 𝐵 ∈ V | 
| 9 |  | rabexg 5336 | . . 3
⊢ (𝐵 ∈ V → {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))} ∈ V) | 
| 10 | 8, 9 | mp1i 13 | . 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))} ∈ V) | 
| 11 |  | fveq2 6905 | . . . . . 6
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) | 
| 12 | 11, 3 | eqtr4di 2794 | . . . . 5
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = 𝐵) | 
| 13 | 12 | adantr 480 | . . . 4
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (Base‘𝑚) = 𝐵) | 
| 14 |  | 2fveq3 6910 | . . . . . . . 8
⊢ (𝑚 = 𝑀 → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) | 
| 16 |  | lcoop.r | . . . . . . . 8
⊢ 𝑅 = (Base‘𝑆) | 
| 17 |  | lcoop.s | . . . . . . . . 9
⊢ 𝑆 = (Scalar‘𝑀) | 
| 18 | 17 | fveq2i 6908 | . . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) | 
| 19 | 16, 18 | eqtri 2764 | . . . . . . 7
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) | 
| 20 | 15, 19 | eqtr4di 2794 | . . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (Base‘(Scalar‘𝑚)) = 𝑅) | 
| 21 |  | simpr 484 | . . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉) | 
| 22 | 20, 21 | oveq12d 7450 | . . . . 5
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → ((Base‘(Scalar‘𝑚)) ↑m 𝑣) = (𝑅 ↑m 𝑉)) | 
| 23 |  | 2fveq3 6910 | . . . . . . . . 9
⊢ (𝑚 = 𝑀 →
(0g‘(Scalar‘𝑚)) = (0g‘(Scalar‘𝑀))) | 
| 24 | 17 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → 𝑆 = (Scalar‘𝑀)) | 
| 25 | 24 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (Scalar‘𝑀) = 𝑆) | 
| 26 | 25 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑚 = 𝑀 →
(0g‘(Scalar‘𝑀)) = (0g‘𝑆)) | 
| 27 | 23, 26 | eqtrd 2776 | . . . . . . . 8
⊢ (𝑚 = 𝑀 →
(0g‘(Scalar‘𝑚)) = (0g‘𝑆)) | 
| 28 | 27 | adantr 480 | . . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) →
(0g‘(Scalar‘𝑚)) = (0g‘𝑆)) | 
| 29 | 28 | breq2d 5154 | . . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (𝑠 finSupp
(0g‘(Scalar‘𝑚)) ↔ 𝑠 finSupp (0g‘𝑆))) | 
| 30 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑚 = 𝑀 → ( linC ‘𝑚) = ( linC ‘𝑀)) | 
| 31 | 30 | adantr 480 | . . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → ( linC ‘𝑚) = ( linC ‘𝑀)) | 
| 32 |  | eqidd 2737 | . . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → 𝑠 = 𝑠) | 
| 33 | 31, 32, 21 | oveq123d 7453 | . . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (𝑠( linC ‘𝑚)𝑣) = (𝑠( linC ‘𝑀)𝑉)) | 
| 34 | 33 | eqeq2d 2747 | . . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (𝑐 = (𝑠( linC ‘𝑚)𝑣) ↔ 𝑐 = (𝑠( linC ‘𝑀)𝑉))) | 
| 35 | 29, 34 | anbi12d 632 | . . . . 5
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → ((𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣)) ↔ (𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉)))) | 
| 36 | 22, 35 | rexeqbidv 3346 | . . . 4
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → (∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣)) ↔ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉)))) | 
| 37 | 13, 36 | rabeqbidv 3454 | . . 3
⊢ ((𝑚 = 𝑀 ∧ 𝑣 = 𝑉) → {𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))} = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) | 
| 38 | 11 | pweqd 4616 | . . 3
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) | 
| 39 |  | df-lco 48329 | . . 3
⊢  LinCo =
(𝑚 ∈ V, 𝑣 ∈ 𝒫
(Base‘𝑚) ↦
{𝑐 ∈ (Base‘𝑚) ∣ ∃𝑠 ∈
((Base‘(Scalar‘𝑚)) ↑m 𝑣)(𝑠 finSupp
(0g‘(Scalar‘𝑚)) ∧ 𝑐 = (𝑠( linC ‘𝑚)𝑣))}) | 
| 40 | 37, 38, 39 | ovmpox 7587 | . 2
⊢ ((𝑀 ∈ V ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))} ∈ V) → (𝑀 LinCo 𝑉) = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) | 
| 41 | 2, 7, 10, 40 | syl3anc 1372 | 1
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 LinCo 𝑉) = {𝑐 ∈ 𝐵 ∣ ∃𝑠 ∈ (𝑅 ↑m 𝑉)(𝑠 finSupp (0g‘𝑆) ∧ 𝑐 = (𝑠( linC ‘𝑀)𝑉))}) |