Step | Hyp | Ref
| Expression |
1 | | lflsccl.v |
. . 3
⊢ 𝑉 = (Base‘𝑊) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) |
3 | | eqidd 2623 |
. 2
⊢ (𝜑 → (+g‘𝑊) = (+g‘𝑊)) |
4 | | lflsccl.d |
. . 3
⊢ 𝐷 = (Scalar‘𝑊) |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → 𝐷 = (Scalar‘𝑊)) |
6 | | eqidd 2623 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊)) |
7 | | lflsccl.k |
. . 3
⊢ 𝐾 = (Base‘𝐷) |
8 | 7 | a1i 11 |
. 2
⊢ (𝜑 → 𝐾 = (Base‘𝐷)) |
9 | | eqidd 2623 |
. 2
⊢ (𝜑 → (+g‘𝐷) = (+g‘𝐷)) |
10 | | lflsccl.t |
. . 3
⊢ · =
(.r‘𝐷) |
11 | 10 | a1i 11 |
. 2
⊢ (𝜑 → · =
(.r‘𝐷)) |
12 | | lflsccl.f |
. . 3
⊢ 𝐹 = (LFnl‘𝑊) |
13 | 12 | a1i 11 |
. 2
⊢ (𝜑 → 𝐹 = (LFnl‘𝑊)) |
14 | | lflsccl.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
15 | 4 | lmodring 18871 |
. . . . 5
⊢ (𝑊 ∈ LMod → 𝐷 ∈ Ring) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Ring) |
17 | 7, 10 | ringcl 18561 |
. . . . 5
⊢ ((𝐷 ∈ Ring ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑥 · 𝑦) ∈ 𝐾) |
18 | 17 | 3expb 1266 |
. . . 4
⊢ ((𝐷 ∈ Ring ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥 · 𝑦) ∈ 𝐾) |
19 | 16, 18 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥 · 𝑦) ∈ 𝐾) |
20 | | lflsccl.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
21 | 4, 7, 1, 12 | lflf 34350 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶𝐾) |
22 | 14, 20, 21 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝐺:𝑉⟶𝐾) |
23 | | lflsccl.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝐾) |
24 | | fconst6g 6094 |
. . . 4
⊢ (𝑅 ∈ 𝐾 → (𝑉 × {𝑅}):𝑉⟶𝐾) |
25 | 23, 24 | syl 17 |
. . 3
⊢ (𝜑 → (𝑉 × {𝑅}):𝑉⟶𝐾) |
26 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝑊)
∈ V |
27 | 1, 26 | eqeltri 2697 |
. . . 4
⊢ 𝑉 ∈ V |
28 | 27 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑉 ∈ V) |
29 | | inidm 3822 |
. . 3
⊢ (𝑉 ∩ 𝑉) = 𝑉 |
30 | 19, 22, 25, 28, 28, 29 | off 6912 |
. 2
⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × {𝑅})):𝑉⟶𝐾) |
31 | 14 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑊 ∈ LMod) |
32 | 20 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝐺 ∈ 𝐹) |
33 | | simpr1 1067 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑟 ∈ 𝐾) |
34 | | simpr2 1068 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝑉) |
35 | | simpr3 1069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ 𝑉) |
36 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) |
37 | | eqid 2622 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
38 | | eqid 2622 |
. . . . . . 7
⊢
(+g‘𝐷) = (+g‘𝐷) |
39 | 1, 36, 4, 37, 7, 38, 10, 12 | lfli 34348 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟 · (𝐺‘𝑥))(+g‘𝐷)(𝐺‘𝑦))) |
40 | 31, 32, 33, 34, 35, 39 | syl113anc 1338 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟 · (𝐺‘𝑥))(+g‘𝐷)(𝐺‘𝑦))) |
41 | 40 | oveq1d 6665 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) · 𝑅) = (((𝑟 · (𝐺‘𝑥))(+g‘𝐷)(𝐺‘𝑦)) · 𝑅)) |
42 | 16 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝐷 ∈ Ring) |
43 | 4, 7, 1, 12 | lflcl 34351 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾) |
44 | 31, 32, 34, 43 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐺‘𝑥) ∈ 𝐾) |
45 | 7, 10 | ringcl 18561 |
. . . . . 6
⊢ ((𝐷 ∈ Ring ∧ 𝑟 ∈ 𝐾 ∧ (𝐺‘𝑥) ∈ 𝐾) → (𝑟 · (𝐺‘𝑥)) ∈ 𝐾) |
46 | 42, 33, 44, 45 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑟 · (𝐺‘𝑥)) ∈ 𝐾) |
47 | 4, 7, 1, 12 | lflcl 34351 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ 𝑉) → (𝐺‘𝑦) ∈ 𝐾) |
48 | 31, 32, 35, 47 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐺‘𝑦) ∈ 𝐾) |
49 | 23 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑅 ∈ 𝐾) |
50 | 7, 38, 10 | ringdir 18567 |
. . . . 5
⊢ ((𝐷 ∈ Ring ∧ ((𝑟 · (𝐺‘𝑥)) ∈ 𝐾 ∧ (𝐺‘𝑦) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → (((𝑟 · (𝐺‘𝑥))(+g‘𝐷)(𝐺‘𝑦)) · 𝑅) = (((𝑟 · (𝐺‘𝑥)) · 𝑅)(+g‘𝐷)((𝐺‘𝑦) · 𝑅))) |
51 | 42, 46, 48, 49, 50 | syl13anc 1328 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (((𝑟 · (𝐺‘𝑥))(+g‘𝐷)(𝐺‘𝑦)) · 𝑅) = (((𝑟 · (𝐺‘𝑥)) · 𝑅)(+g‘𝐷)((𝐺‘𝑦) · 𝑅))) |
52 | 7, 10 | ringass 18564 |
. . . . . 6
⊢ ((𝐷 ∈ Ring ∧ (𝑟 ∈ 𝐾 ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑟 · (𝐺‘𝑥)) · 𝑅) = (𝑟 · ((𝐺‘𝑥) · 𝑅))) |
53 | 42, 33, 44, 49, 52 | syl13anc 1328 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟 · (𝐺‘𝑥)) · 𝑅) = (𝑟 · ((𝐺‘𝑥) · 𝑅))) |
54 | 53 | oveq1d 6665 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (((𝑟 · (𝐺‘𝑥)) · 𝑅)(+g‘𝐷)((𝐺‘𝑦) · 𝑅)) = ((𝑟 · ((𝐺‘𝑥) · 𝑅))(+g‘𝐷)((𝐺‘𝑦) · 𝑅))) |
55 | 41, 51, 54 | 3eqtrd 2660 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) · 𝑅) = ((𝑟 · ((𝐺‘𝑥) · 𝑅))(+g‘𝐷)((𝐺‘𝑦) · 𝑅))) |
56 | 1, 4, 37, 7 | lmodvscl 18880 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ 𝑉) |
57 | 31, 33, 34, 56 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ 𝑉) |
58 | 1, 36 | lmodvacl 18877 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉) |
59 | 31, 57, 35, 58 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉) |
60 | | ffn 6045 |
. . . . . 6
⊢ (𝐺:𝑉⟶𝐾 → 𝐺 Fn 𝑉) |
61 | 22, 60 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 Fn 𝑉) |
62 | | eqidd 2623 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦))) |
63 | 28, 23, 61, 62 | ofc2 6921 |
. . . 4
⊢ ((𝜑 ∧ ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) · 𝑅)) |
64 | 59, 63 | syldan 487 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) · 𝑅)) |
65 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
66 | 28, 23, 61, 65 | ofc2 6921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑥) = ((𝐺‘𝑥) · 𝑅)) |
67 | 34, 66 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑥) = ((𝐺‘𝑥) · 𝑅)) |
68 | 67 | oveq2d 6666 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑟 · ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑥)) = (𝑟 · ((𝐺‘𝑥) · 𝑅))) |
69 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
70 | 28, 23, 61, 69 | ofc2 6921 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑦) = ((𝐺‘𝑦) · 𝑅)) |
71 | 35, 70 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑦) = ((𝐺‘𝑦) · 𝑅)) |
72 | 68, 71 | oveq12d 6668 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑟 · ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑥))(+g‘𝐷)((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑦)) = ((𝑟 · ((𝐺‘𝑥) · 𝑅))(+g‘𝐷)((𝐺‘𝑦) · 𝑅))) |
73 | 55, 64, 72 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ (𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟 · ((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑥))(+g‘𝐷)((𝐺 ∘𝑓 · (𝑉 × {𝑅}))‘𝑦))) |
74 | 2, 3, 5, 6, 8, 9, 11, 13, 30, 73, 14 | islfld 34349 |
1
⊢ (𝜑 → (𝐺 ∘𝑓 · (𝑉 × {𝑅})) ∈ 𝐹) |