| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lflnegcl.w | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 2 |  | lflnegcl.r | . . . . . . . 8
⊢ 𝑅 = (Scalar‘𝑊) | 
| 3 | 2 | lmodring 20866 | . . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Ring) | 
| 4 | 1, 3 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 5 |  | ringgrp 20235 | . . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 6 | 4, 5 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 7 | 6 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑅 ∈ Grp) | 
| 8 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod) | 
| 9 |  | lflnegcl.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐹) | 
| 10 | 9 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹) | 
| 11 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) | 
| 12 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 13 |  | lflnegcl.v | . . . . . 6
⊢ 𝑉 = (Base‘𝑊) | 
| 14 |  | lflnegcl.f | . . . . . 6
⊢ 𝐹 = (LFnl‘𝑊) | 
| 15 | 2, 12, 13, 14 | lflcl 39065 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ (Base‘𝑅)) | 
| 16 | 8, 10, 11, 15 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ (Base‘𝑅)) | 
| 17 |  | lflnegcl.i | . . . . 5
⊢ 𝐼 = (invg‘𝑅) | 
| 18 | 12, 17 | grpinvcl 19005 | . . . 4
⊢ ((𝑅 ∈ Grp ∧ (𝐺‘𝑥) ∈ (Base‘𝑅)) → (𝐼‘(𝐺‘𝑥)) ∈ (Base‘𝑅)) | 
| 19 | 7, 16, 18 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐼‘(𝐺‘𝑥)) ∈ (Base‘𝑅)) | 
| 20 |  | lflnegcl.n | . . 3
⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥))) | 
| 21 | 19, 20 | fmptd 7134 | . 2
⊢ (𝜑 → 𝑁:𝑉⟶(Base‘𝑅)) | 
| 22 |  | ringabl 20278 | . . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel) | 
| 23 | 4, 22 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Abel) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑅 ∈ Abel) | 
| 25 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑅 ∈ Ring) | 
| 26 |  | simpr1 1195 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑘 ∈ (Base‘𝑅)) | 
| 27 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑊 ∈ LMod) | 
| 28 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝐺 ∈ 𝐹) | 
| 29 |  | simpr2 1196 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑦 ∈ 𝑉) | 
| 30 | 2, 12, 13, 14 | lflcl 39065 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ 𝑉) → (𝐺‘𝑦) ∈ (Base‘𝑅)) | 
| 31 | 27, 28, 29, 30 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘𝑦) ∈ (Base‘𝑅)) | 
| 32 |  | eqid 2737 | . . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 33 | 12, 32 | ringcl 20247 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (Base‘𝑅) ∧ (𝐺‘𝑦) ∈ (Base‘𝑅)) → (𝑘(.r‘𝑅)(𝐺‘𝑦)) ∈ (Base‘𝑅)) | 
| 34 | 25, 26, 31, 33 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘(.r‘𝑅)(𝐺‘𝑦)) ∈ (Base‘𝑅)) | 
| 35 |  | simpr3 1197 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉) | 
| 36 | 2, 12, 13, 14 | lflcl 39065 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐺‘𝑧) ∈ (Base‘𝑅)) | 
| 37 | 27, 28, 35, 36 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘𝑧) ∈ (Base‘𝑅)) | 
| 38 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 39 | 12, 38, 17 | ablinvadd 19825 | . . . . . 6
⊢ ((𝑅 ∈ Abel ∧ (𝑘(.r‘𝑅)(𝐺‘𝑦)) ∈ (Base‘𝑅) ∧ (𝐺‘𝑧) ∈ (Base‘𝑅)) → (𝐼‘((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) = ((𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) | 
| 40 | 24, 34, 37, 39 | syl3anc 1373 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐼‘((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) = ((𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) | 
| 41 |  | eqid 2737 | . . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 42 |  | eqid 2737 | . . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 43 | 13, 41, 2, 42, 12, 38, 32, 14 | lfli 39062 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) | 
| 44 | 27, 28, 26, 29, 35, 43 | syl113anc 1384 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) | 
| 45 | 44 | fveq2d 6910 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) = (𝐼‘((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧)))) | 
| 46 | 12, 32, 17, 25, 26, 31 | ringmneg2 20302 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦))) = (𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))) | 
| 47 | 46 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧))) = ((𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) | 
| 48 | 40, 45, 47 | 3eqtr4d 2787 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) = ((𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) | 
| 49 | 13, 2, 42, 12 | lmodvscl 20876 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) | 
| 50 | 27, 26, 29, 49 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) | 
| 51 | 13, 41 | lmodvacl 20873 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) | 
| 52 | 27, 50, 35, 51 | syl3anc 1373 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) | 
| 53 |  | 2fveq3 6911 | . . . . . 6
⊢ (𝑥 = ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) → (𝐼‘(𝐺‘𝑥)) = (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) | 
| 54 |  | fvex 6919 | . . . . . 6
⊢ (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) ∈ V | 
| 55 | 53, 20, 54 | fvmpt 7016 | . . . . 5
⊢ (((𝑘(
·𝑠 ‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉 → (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) | 
| 56 | 52, 55 | syl 17 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) | 
| 57 |  | 2fveq3 6911 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐼‘(𝐺‘𝑥)) = (𝐼‘(𝐺‘𝑦))) | 
| 58 |  | fvex 6919 | . . . . . . . 8
⊢ (𝐼‘(𝐺‘𝑦)) ∈ V | 
| 59 | 57, 20, 58 | fvmpt 7016 | . . . . . . 7
⊢ (𝑦 ∈ 𝑉 → (𝑁‘𝑦) = (𝐼‘(𝐺‘𝑦))) | 
| 60 | 29, 59 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘𝑦) = (𝐼‘(𝐺‘𝑦))) | 
| 61 | 60 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘(.r‘𝑅)(𝑁‘𝑦)) = (𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))) | 
| 62 |  | 2fveq3 6911 | . . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐼‘(𝐺‘𝑥)) = (𝐼‘(𝐺‘𝑧))) | 
| 63 |  | fvex 6919 | . . . . . . 7
⊢ (𝐼‘(𝐺‘𝑧)) ∈ V | 
| 64 | 62, 20, 63 | fvmpt 7016 | . . . . . 6
⊢ (𝑧 ∈ 𝑉 → (𝑁‘𝑧) = (𝐼‘(𝐺‘𝑧))) | 
| 65 | 35, 64 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘𝑧) = (𝐼‘(𝐺‘𝑧))) | 
| 66 | 61, 65 | oveq12d 7449 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧)) = ((𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) | 
| 67 | 48, 56, 66 | 3eqtr4d 2787 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))) | 
| 68 | 67 | ralrimivvva 3205 | . 2
⊢ (𝜑 → ∀𝑘 ∈ (Base‘𝑅)∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))) | 
| 69 | 13, 41, 2, 42, 12, 38, 32, 14 | islfl 39061 | . . 3
⊢ (𝑊 ∈ LMod → (𝑁 ∈ 𝐹 ↔ (𝑁:𝑉⟶(Base‘𝑅) ∧ ∀𝑘 ∈ (Base‘𝑅)∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))))) | 
| 70 | 1, 69 | syl 17 | . 2
⊢ (𝜑 → (𝑁 ∈ 𝐹 ↔ (𝑁:𝑉⟶(Base‘𝑅) ∧ ∀𝑘 ∈ (Base‘𝑅)∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))))) | 
| 71 | 21, 68, 70 | mpbir2and 713 | 1
⊢ (𝜑 → 𝑁 ∈ 𝐹) |