| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp11 1204 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝜑) | 
| 2 |  | simp12 1205 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑡 ∈ 𝒫 𝐵) | 
| 3 | 2 | elpwid 4609 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑡 ⊆ 𝐵) | 
| 4 |  | simp2 1138 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑥 ∈ 𝑡) | 
| 5 | 3, 4 | sseldd 3984 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑥 ∈ 𝐵) | 
| 6 |  | simp13 1206 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑢 ∈ 𝒫 𝐵) | 
| 7 | 6 | elpwid 4609 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑢 ⊆ 𝐵) | 
| 8 |  | simp3 1139 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑦 ∈ 𝑢) | 
| 9 | 7, 8 | sseldd 3984 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → 𝑦 ∈ 𝐵) | 
| 10 |  | lsmpropd.p | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) | 
| 11 | 1, 5, 9, 10 | syl12anc 837 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑡 ∧ 𝑦 ∈ 𝑢) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) | 
| 12 | 11 | mpoeq3dva 7510 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) → (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦)) = (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦))) | 
| 13 | 12 | rneqd 5949 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑢 ∈ 𝒫 𝐵) → ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦)) = ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦))) | 
| 14 | 13 | mpoeq3dva 7510 | . . 3
⊢ (𝜑 → (𝑡 ∈ 𝒫 𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦))) = (𝑡 ∈ 𝒫 𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦)))) | 
| 15 |  | lsmpropd.b1 | . . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) | 
| 16 | 15 | pweqd 4617 | . . . 4
⊢ (𝜑 → 𝒫 𝐵 = 𝒫 (Base‘𝐾)) | 
| 17 |  | mpoeq12 7506 | . . . 4
⊢
((𝒫 𝐵 =
𝒫 (Base‘𝐾)
∧ 𝒫 𝐵 =
𝒫 (Base‘𝐾))
→ (𝑡 ∈ 𝒫
𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦))) = (𝑡 ∈ 𝒫 (Base‘𝐾), 𝑢 ∈ 𝒫 (Base‘𝐾) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦)))) | 
| 18 | 16, 16, 17 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑡 ∈ 𝒫 𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦))) = (𝑡 ∈ 𝒫 (Base‘𝐾), 𝑢 ∈ 𝒫 (Base‘𝐾) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦)))) | 
| 19 |  | lsmpropd.b2 | . . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) | 
| 20 | 19 | pweqd 4617 | . . . 4
⊢ (𝜑 → 𝒫 𝐵 = 𝒫 (Base‘𝐿)) | 
| 21 |  | mpoeq12 7506 | . . . 4
⊢
((𝒫 𝐵 =
𝒫 (Base‘𝐿)
∧ 𝒫 𝐵 =
𝒫 (Base‘𝐿))
→ (𝑡 ∈ 𝒫
𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦))) = (𝑡 ∈ 𝒫 (Base‘𝐿), 𝑢 ∈ 𝒫 (Base‘𝐿) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦)))) | 
| 22 | 20, 20, 21 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑡 ∈ 𝒫 𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦))) = (𝑡 ∈ 𝒫 (Base‘𝐿), 𝑢 ∈ 𝒫 (Base‘𝐿) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦)))) | 
| 23 | 14, 18, 22 | 3eqtr3d 2785 | . 2
⊢ (𝜑 → (𝑡 ∈ 𝒫 (Base‘𝐾), 𝑢 ∈ 𝒫 (Base‘𝐾) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦))) = (𝑡 ∈ 𝒫 (Base‘𝐿), 𝑢 ∈ 𝒫 (Base‘𝐿) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦)))) | 
| 24 |  | lsmpropd.v1 | . . 3
⊢ (𝜑 → 𝐾 ∈ 𝑉) | 
| 25 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 26 |  | eqid 2737 | . . . 4
⊢
(+g‘𝐾) = (+g‘𝐾) | 
| 27 |  | eqid 2737 | . . . 4
⊢
(LSSum‘𝐾) =
(LSSum‘𝐾) | 
| 28 | 25, 26, 27 | lsmfval 19656 | . . 3
⊢ (𝐾 ∈ 𝑉 → (LSSum‘𝐾) = (𝑡 ∈ 𝒫 (Base‘𝐾), 𝑢 ∈ 𝒫 (Base‘𝐾) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦)))) | 
| 29 | 24, 28 | syl 17 | . 2
⊢ (𝜑 → (LSSum‘𝐾) = (𝑡 ∈ 𝒫 (Base‘𝐾), 𝑢 ∈ 𝒫 (Base‘𝐾) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐾)𝑦)))) | 
| 30 |  | lsmpropd.v2 | . . 3
⊢ (𝜑 → 𝐿 ∈ 𝑊) | 
| 31 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐿) =
(Base‘𝐿) | 
| 32 |  | eqid 2737 | . . . 4
⊢
(+g‘𝐿) = (+g‘𝐿) | 
| 33 |  | eqid 2737 | . . . 4
⊢
(LSSum‘𝐿) =
(LSSum‘𝐿) | 
| 34 | 31, 32, 33 | lsmfval 19656 | . . 3
⊢ (𝐿 ∈ 𝑊 → (LSSum‘𝐿) = (𝑡 ∈ 𝒫 (Base‘𝐿), 𝑢 ∈ 𝒫 (Base‘𝐿) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦)))) | 
| 35 | 30, 34 | syl 17 | . 2
⊢ (𝜑 → (LSSum‘𝐿) = (𝑡 ∈ 𝒫 (Base‘𝐿), 𝑢 ∈ 𝒫 (Base‘𝐿) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝐿)𝑦)))) | 
| 36 | 23, 29, 35 | 3eqtr4d 2787 | 1
⊢ (𝜑 → (LSSum‘𝐾) = (LSSum‘𝐿)) |