| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ldualgrp.f | . . . 4
⊢ 𝐹 = (LFnl‘𝑊) | 
| 2 |  | ldualgrp.d | . . . 4
⊢ 𝐷 = (LDual‘𝑊) | 
| 3 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 4 |  | ldualgrp.w | . . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 5 | 1, 2, 3, 4 | ldualvbase 39127 | . . 3
⊢ (𝜑 → (Base‘𝐷) = 𝐹) | 
| 6 | 5 | eqcomd 2743 | . 2
⊢ (𝜑 → 𝐹 = (Base‘𝐷)) | 
| 7 |  | eqidd 2738 | . 2
⊢ (𝜑 → (+g‘𝐷) = (+g‘𝐷)) | 
| 8 |  | eqid 2737 | . . 3
⊢
(+g‘𝐷) = (+g‘𝐷) | 
| 9 | 4 | 3ad2ant1 1134 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → 𝑊 ∈ LMod) | 
| 10 |  | simp2 1138 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → 𝑥 ∈ 𝐹) | 
| 11 |  | simp3 1139 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → 𝑦 ∈ 𝐹) | 
| 12 | 1, 2, 8, 9, 10, 11 | ldualvaddcl 39131 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥(+g‘𝐷)𝑦) ∈ 𝐹) | 
| 13 |  | ldualgrp.r | . . . . 5
⊢ 𝑅 = (Scalar‘𝑊) | 
| 14 |  | eqid 2737 | . . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 15 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → 𝑊 ∈ LMod) | 
| 16 |  | simpr2 1196 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → 𝑦 ∈ 𝐹) | 
| 17 |  | simpr3 1197 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → 𝑧 ∈ 𝐹) | 
| 18 | 1, 13, 14, 2, 8, 15, 16, 17 | ldualvadd 39130 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → (𝑦(+g‘𝐷)𝑧) = (𝑦 ∘f
(+g‘𝑅)𝑧)) | 
| 19 | 18 | oveq2d 7447 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → (𝑥 ∘f
(+g‘𝑅)(𝑦(+g‘𝐷)𝑧)) = (𝑥 ∘f
(+g‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧))) | 
| 20 |  | simpr1 1195 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → 𝑥 ∈ 𝐹) | 
| 21 | 1, 2, 8, 15, 16, 17 | ldualvaddcl 39131 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → (𝑦(+g‘𝐷)𝑧) ∈ 𝐹) | 
| 22 | 1, 13, 14, 2, 8, 15, 20, 21 | ldualvadd 39130 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → (𝑥(+g‘𝐷)(𝑦(+g‘𝐷)𝑧)) = (𝑥 ∘f
(+g‘𝑅)(𝑦(+g‘𝐷)𝑧))) | 
| 23 | 1, 2, 8, 15, 20, 16 | ldualvaddcl 39131 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → (𝑥(+g‘𝐷)𝑦) ∈ 𝐹) | 
| 24 | 1, 13, 14, 2, 8, 15, 23, 17 | ldualvadd 39130 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → ((𝑥(+g‘𝐷)𝑦)(+g‘𝐷)𝑧) = ((𝑥(+g‘𝐷)𝑦) ∘f
(+g‘𝑅)𝑧)) | 
| 25 | 1, 13, 14, 2, 8, 15, 20, 16 | ldualvadd 39130 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → (𝑥(+g‘𝐷)𝑦) = (𝑥 ∘f
(+g‘𝑅)𝑦)) | 
| 26 | 25 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → ((𝑥(+g‘𝐷)𝑦) ∘f
(+g‘𝑅)𝑧) = ((𝑥 ∘f
(+g‘𝑅)𝑦) ∘f
(+g‘𝑅)𝑧)) | 
| 27 | 13, 14, 1, 15, 20, 16, 17 | lfladdass 39074 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → ((𝑥 ∘f
(+g‘𝑅)𝑦) ∘f
(+g‘𝑅)𝑧) = (𝑥 ∘f
(+g‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧))) | 
| 28 | 24, 26, 27 | 3eqtrd 2781 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → ((𝑥(+g‘𝐷)𝑦)(+g‘𝐷)𝑧) = (𝑥 ∘f
(+g‘𝑅)(𝑦 ∘f
(+g‘𝑅)𝑧))) | 
| 29 | 19, 22, 28 | 3eqtr4rd 2788 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹)) → ((𝑥(+g‘𝐷)𝑦)(+g‘𝐷)𝑧) = (𝑥(+g‘𝐷)(𝑦(+g‘𝐷)𝑧))) | 
| 30 |  | eqid 2737 | . . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 31 |  | ldualgrp.v | . . . 4
⊢ 𝑉 = (Base‘𝑊) | 
| 32 | 13, 30, 31, 1 | lfl0f 39070 | . . 3
⊢ (𝑊 ∈ LMod → (𝑉 ×
{(0g‘𝑅)})
∈ 𝐹) | 
| 33 | 4, 32 | syl 17 | . 2
⊢ (𝜑 → (𝑉 × {(0g‘𝑅)}) ∈ 𝐹) | 
| 34 | 4 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → 𝑊 ∈ LMod) | 
| 35 | 33 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → (𝑉 × {(0g‘𝑅)}) ∈ 𝐹) | 
| 36 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ 𝐹) | 
| 37 | 1, 13, 14, 2, 8, 34, 35, 36 | ldualvadd 39130 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → ((𝑉 × {(0g‘𝑅)})(+g‘𝐷)𝑥) = ((𝑉 × {(0g‘𝑅)}) ∘f
(+g‘𝑅)𝑥)) | 
| 38 | 31, 13, 14, 30, 1, 34, 36 | lfladd0l 39075 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → ((𝑉 × {(0g‘𝑅)}) ∘f
(+g‘𝑅)𝑥) = 𝑥) | 
| 39 | 37, 38 | eqtrd 2777 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → ((𝑉 × {(0g‘𝑅)})(+g‘𝐷)𝑥) = 𝑥) | 
| 40 |  | eqid 2737 | . . 3
⊢
(invg‘𝑅) = (invg‘𝑅) | 
| 41 |  | eqid 2737 | . . 3
⊢ (𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧))) = (𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧))) | 
| 42 | 31, 13, 40, 41, 1, 34, 36 | lflnegcl 39076 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → (𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧))) ∈ 𝐹) | 
| 43 | 1, 13, 14, 2, 8, 34, 42, 36 | ldualvadd 39130 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → ((𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧)))(+g‘𝐷)𝑥) = ((𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧))) ∘f
(+g‘𝑅)𝑥)) | 
| 44 | 31, 13, 40, 41, 1, 34, 36, 14, 30 | lflnegl 39077 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → ((𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧))) ∘f
(+g‘𝑅)𝑥) = (𝑉 × {(0g‘𝑅)})) | 
| 45 | 43, 44 | eqtrd 2777 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐹) → ((𝑧 ∈ 𝑉 ↦ ((invg‘𝑅)‘(𝑥‘𝑧)))(+g‘𝐷)𝑥) = (𝑉 × {(0g‘𝑅)})) | 
| 46 | 6, 7, 12, 29, 33, 39, 42, 45 | isgrpd 18976 | 1
⊢ (𝜑 → 𝐷 ∈ Grp) |