Step | Hyp | Ref
| Expression |
1 | | lflnegcl.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
2 | | lflnegcl.r |
. . . . . . . 8
⊢ 𝑅 = (Scalar‘𝑊) |
3 | 2 | lmodring 18871 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Ring) |
4 | 1, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | | ringgrp 18552 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑅 ∈ Grp) |
8 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod) |
9 | | lflnegcl.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
10 | 9 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹) |
11 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
12 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | | lflnegcl.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑊) |
14 | | lflnegcl.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑊) |
15 | 2, 12, 13, 14 | lflcl 34351 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ (Base‘𝑅)) |
16 | 8, 10, 11, 15 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ (Base‘𝑅)) |
17 | | lflnegcl.i |
. . . . 5
⊢ 𝐼 = (invg‘𝑅) |
18 | 12, 17 | grpinvcl 17467 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ (𝐺‘𝑥) ∈ (Base‘𝑅)) → (𝐼‘(𝐺‘𝑥)) ∈ (Base‘𝑅)) |
19 | 7, 16, 18 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐼‘(𝐺‘𝑥)) ∈ (Base‘𝑅)) |
20 | | lflnegcl.n |
. . 3
⊢ 𝑁 = (𝑥 ∈ 𝑉 ↦ (𝐼‘(𝐺‘𝑥))) |
21 | 19, 20 | fmptd 6385 |
. 2
⊢ (𝜑 → 𝑁:𝑉⟶(Base‘𝑅)) |
22 | | ringabl 18580 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel) |
23 | 4, 22 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Abel) |
24 | 23 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑅 ∈ Abel) |
25 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑅 ∈ Ring) |
26 | | simpr1 1067 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑘 ∈ (Base‘𝑅)) |
27 | 1 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑊 ∈ LMod) |
28 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝐺 ∈ 𝐹) |
29 | | simpr2 1068 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑦 ∈ 𝑉) |
30 | 2, 12, 13, 14 | lflcl 34351 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ 𝑉) → (𝐺‘𝑦) ∈ (Base‘𝑅)) |
31 | 27, 28, 29, 30 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘𝑦) ∈ (Base‘𝑅)) |
32 | | eqid 2622 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
33 | 12, 32 | ringcl 18561 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (Base‘𝑅) ∧ (𝐺‘𝑦) ∈ (Base‘𝑅)) → (𝑘(.r‘𝑅)(𝐺‘𝑦)) ∈ (Base‘𝑅)) |
34 | 25, 26, 31, 33 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘(.r‘𝑅)(𝐺‘𝑦)) ∈ (Base‘𝑅)) |
35 | | simpr3 1069 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉) |
36 | 2, 12, 13, 14 | lflcl 34351 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐺‘𝑧) ∈ (Base‘𝑅)) |
37 | 27, 28, 35, 36 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘𝑧) ∈ (Base‘𝑅)) |
38 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
39 | 12, 38, 17 | ablinvadd 18215 |
. . . . . 6
⊢ ((𝑅 ∈ Abel ∧ (𝑘(.r‘𝑅)(𝐺‘𝑦)) ∈ (Base‘𝑅) ∧ (𝐺‘𝑧) ∈ (Base‘𝑅)) → (𝐼‘((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) = ((𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) |
40 | 24, 34, 37, 39 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐼‘((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) = ((𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) |
41 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) |
42 | | eqid 2622 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
43 | 13, 41, 2, 42, 12, 38, 32, 14 | lfli 34348 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) |
44 | 27, 28, 26, 29, 35, 43 | syl113anc 1338 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧))) |
45 | 44 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) = (𝐼‘((𝑘(.r‘𝑅)(𝐺‘𝑦))(+g‘𝑅)(𝐺‘𝑧)))) |
46 | 12, 32, 17, 25, 26, 31 | ringmneg2 18597 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦))) = (𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))) |
47 | 46 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧))) = ((𝐼‘(𝑘(.r‘𝑅)(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) |
48 | 40, 45, 47 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) = ((𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) |
49 | 13, 2, 42, 12 | lmodvscl 18880 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
50 | 27, 26, 29, 49 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
51 | 13, 41 | lmodvacl 18877 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) |
52 | 27, 50, 35, 51 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) |
53 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) → (𝐺‘𝑥) = (𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) |
54 | 53 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = ((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) → (𝐼‘(𝐺‘𝑥)) = (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) |
55 | | fvex 6201 |
. . . . . 6
⊢ (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) ∈ V |
56 | 54, 20, 55 | fvmpt 6282 |
. . . . 5
⊢ (((𝑘(
·𝑠 ‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉 → (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) |
57 | 52, 56 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = (𝐼‘(𝐺‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) |
58 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
59 | 58 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐼‘(𝐺‘𝑥)) = (𝐼‘(𝐺‘𝑦))) |
60 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐼‘(𝐺‘𝑦)) ∈ V |
61 | 59, 20, 60 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑉 → (𝑁‘𝑦) = (𝐼‘(𝐺‘𝑦))) |
62 | 29, 61 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘𝑦) = (𝐼‘(𝐺‘𝑦))) |
63 | 62 | oveq2d 6666 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑘(.r‘𝑅)(𝑁‘𝑦)) = (𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))) |
64 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
65 | 64 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝐼‘(𝐺‘𝑥)) = (𝐼‘(𝐺‘𝑧))) |
66 | | fvex 6201 |
. . . . . . 7
⊢ (𝐼‘(𝐺‘𝑧)) ∈ V |
67 | 65, 20, 66 | fvmpt 6282 |
. . . . . 6
⊢ (𝑧 ∈ 𝑉 → (𝑁‘𝑧) = (𝐼‘(𝐺‘𝑧))) |
68 | 35, 67 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘𝑧) = (𝐼‘(𝐺‘𝑧))) |
69 | 63, 68 | oveq12d 6668 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧)) = ((𝑘(.r‘𝑅)(𝐼‘(𝐺‘𝑦)))(+g‘𝑅)(𝐼‘(𝐺‘𝑧)))) |
70 | 48, 57, 69 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))) |
71 | 70 | ralrimivvva 2972 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (Base‘𝑅)∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))) |
72 | 13, 41, 2, 42, 12, 38, 32, 14 | islfl 34347 |
. . 3
⊢ (𝑊 ∈ LMod → (𝑁 ∈ 𝐹 ↔ (𝑁:𝑉⟶(Base‘𝑅) ∧ ∀𝑘 ∈ (Base‘𝑅)∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))))) |
73 | 1, 72 | syl 17 |
. 2
⊢ (𝜑 → (𝑁 ∈ 𝐹 ↔ (𝑁:𝑉⟶(Base‘𝑅) ∧ ∀𝑘 ∈ (Base‘𝑅)∀𝑦 ∈ 𝑉 ∀𝑧 ∈ 𝑉 (𝑁‘((𝑘( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑘(.r‘𝑅)(𝑁‘𝑦))(+g‘𝑅)(𝑁‘𝑧))))) |
74 | 21, 71, 73 | mpbir2and 957 |
1
⊢ (𝜑 → 𝑁 ∈ 𝐹) |