Step | Hyp | Ref
| Expression |
1 | | lflsccl.v |
. . 3
β’ π = (Baseβπ) |
2 | 1 | a1i 11 |
. 2
β’ (π β π = (Baseβπ)) |
3 | | eqidd 2734 |
. 2
β’ (π β (+gβπ) = (+gβπ)) |
4 | | lflsccl.d |
. . 3
β’ π· = (Scalarβπ) |
5 | 4 | a1i 11 |
. 2
β’ (π β π· = (Scalarβπ)) |
6 | | eqidd 2734 |
. 2
β’ (π β (
Β·π βπ) = ( Β·π
βπ)) |
7 | | lflsccl.k |
. . 3
β’ πΎ = (Baseβπ·) |
8 | 7 | a1i 11 |
. 2
β’ (π β πΎ = (Baseβπ·)) |
9 | | eqidd 2734 |
. 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 20344 |
. . . . 5
β’ (π β LMod β π· β Ring) |
16 | 14, 15 | syl 17 |
. . . 4
β’ (π β π· β Ring) |
17 | 7, 10 | ringcl 19986 |
. . . . 5
β’ ((π· β Ring β§ π₯ β πΎ β§ π¦ β πΎ) β (π₯ Β· π¦) β πΎ) |
18 | 17 | 3expb 1121 |
. . . 4
β’ ((π· β Ring β§ (π₯ β πΎ β§ π¦ β πΎ)) β (π₯ Β· π¦) β πΎ) |
19 | 16, 18 | sylan 581 |
. . 3
β’ ((π β§ (π₯ β πΎ β§ π¦ β πΎ)) β (π₯ Β· π¦) β πΎ) |
20 | | lflsccl.g |
. . . 4
β’ (π β πΊ β πΉ) |
21 | 4, 7, 1, 12 | lflf 37571 |
. . . 4
β’ ((π β LMod β§ πΊ β πΉ) β πΊ:πβΆπΎ) |
22 | 14, 20, 21 | syl2anc 585 |
. . 3
β’ (π β πΊ:πβΆπΎ) |
23 | | lflsccl.r |
. . . 4
β’ (π β π
β πΎ) |
24 | | fconst6g 6732 |
. . . 4
β’ (π
β πΎ β (π Γ {π
}):πβΆπΎ) |
25 | 23, 24 | syl 17 |
. . 3
β’ (π β (π Γ {π
}):πβΆπΎ) |
26 | 1 | fvexi 6857 |
. . . 4
β’ π β V |
27 | 26 | a1i 11 |
. . 3
β’ (π β π β V) |
28 | | inidm 4179 |
. . 3
β’ (π β© π) = π |
29 | 19, 22, 25, 27, 27, 28 | off 7636 |
. 2
β’ (π β (πΊ βf Β· (π Γ {π
})):πβΆπΎ) |
30 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β π β LMod) |
31 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β πΊ β πΉ) |
32 | | simpr1 1195 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β π β πΎ) |
33 | | simpr2 1196 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β π₯ β π) |
34 | | simpr3 1197 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β π¦ β π) |
35 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
36 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
37 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ·) = (+gβπ·) |
38 | 1, 35, 4, 36, 7, 37, 10, 12 | lfli 37569 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π Β· (πΊβπ₯))(+gβπ·)(πΊβπ¦))) |
39 | 30, 31, 32, 33, 34, 38 | syl113anc 1383 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π Β· (πΊβπ₯))(+gβπ·)(πΊβπ¦))) |
40 | 39 | oveq1d 7373 |
. . . 4
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) Β· π
) = (((π Β· (πΊβπ₯))(+gβπ·)(πΊβπ¦)) Β· π
)) |
41 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β π· β Ring) |
42 | 4, 7, 1, 12 | lflcl 37572 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ π₯ β π) β (πΊβπ₯) β πΎ) |
43 | 30, 31, 33, 42 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (πΊβπ₯) β πΎ) |
44 | 7, 10 | ringcl 19986 |
. . . . . 6
β’ ((π· β Ring β§ π β πΎ β§ (πΊβπ₯) β πΎ) β (π Β· (πΊβπ₯)) β πΎ) |
45 | 41, 32, 43, 44 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (π Β· (πΊβπ₯)) β πΎ) |
46 | 4, 7, 1, 12 | lflcl 37572 |
. . . . . 6
β’ ((π β LMod β§ πΊ β πΉ β§ π¦ β π) β (πΊβπ¦) β πΎ) |
47 | 30, 31, 34, 46 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (πΊβπ¦) β πΎ) |
48 | 23 | adantr 482 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β π
β πΎ) |
49 | 7, 37, 10 | ringdir 19993 |
. . . . 5
β’ ((π· β Ring β§ ((π Β· (πΊβπ₯)) β πΎ β§ (πΊβπ¦) β πΎ β§ π
β πΎ)) β (((π Β· (πΊβπ₯))(+gβπ·)(πΊβπ¦)) Β· π
) = (((π Β· (πΊβπ₯)) Β· π
)(+gβπ·)((πΊβπ¦) Β· π
))) |
50 | 41, 45, 47, 48, 49 | syl13anc 1373 |
. . . 4
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (((π Β· (πΊβπ₯))(+gβπ·)(πΊβπ¦)) Β· π
) = (((π Β· (πΊβπ₯)) Β· π
)(+gβπ·)((πΊβπ¦) Β· π
))) |
51 | 7, 10 | ringass 19989 |
. . . . . 6
β’ ((π· β Ring β§ (π β πΎ β§ (πΊβπ₯) β πΎ β§ π
β πΎ)) β ((π Β· (πΊβπ₯)) Β· π
) = (π Β· ((πΊβπ₯) Β· π
))) |
52 | 41, 32, 43, 48, 51 | syl13anc 1373 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((π Β· (πΊβπ₯)) Β· π
) = (π Β· ((πΊβπ₯) Β· π
))) |
53 | 52 | oveq1d 7373 |
. . . 4
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (((π Β· (πΊβπ₯)) Β· π
)(+gβπ·)((πΊβπ¦) Β· π
)) = ((π Β· ((πΊβπ₯) Β· π
))(+gβπ·)((πΊβπ¦) Β· π
))) |
54 | 40, 50, 53 | 3eqtrd 2777 |
. . 3
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) Β· π
) = ((π Β· ((πΊβπ₯) Β· π
))(+gβπ·)((πΊβπ¦) Β· π
))) |
55 | 1, 4, 36, 7 | lmodvscl 20354 |
. . . . . 6
β’ ((π β LMod β§ π β πΎ β§ π₯ β π) β (π( Β·π
βπ)π₯) β π) |
56 | 30, 32, 33, 55 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (π( Β·π
βπ)π₯) β π) |
57 | 1, 35 | lmodvacl 20351 |
. . . . 5
β’ ((π β LMod β§ (π(
Β·π βπ)π₯) β π β§ π¦ β π) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β π) |
58 | 30, 56, 34, 57 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β π) |
59 | 22 | ffnd 6670 |
. . . . 5
β’ (π β πΊ Fn π) |
60 | | eqidd 2734 |
. . . . 5
β’ ((π β§ ((π( Β·π
βπ)π₯)(+gβπ)π¦) β π) β (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) = (πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦))) |
61 | 27, 23, 59, 60 | ofc2 7645 |
. . . 4
β’ ((π β§ ((π( Β·π
βπ)π₯)(+gβπ)π¦) β π) β ((πΊ βf Β· (π Γ {π
}))β((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) Β· π
)) |
62 | 58, 61 | syldan 592 |
. . 3
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((πΊ βf Β· (π Γ {π
}))β((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((πΊβ((π( Β·π
βπ)π₯)(+gβπ)π¦)) Β· π
)) |
63 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πΊβπ₯) = (πΊβπ₯)) |
64 | 27, 23, 59, 63 | ofc2 7645 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((πΊ βf Β· (π Γ {π
}))βπ₯) = ((πΊβπ₯) Β· π
)) |
65 | 33, 64 | syldan 592 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((πΊ βf Β· (π Γ {π
}))βπ₯) = ((πΊβπ₯) Β· π
)) |
66 | 65 | oveq2d 7374 |
. . . 4
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (π Β· ((πΊ βf Β· (π Γ {π
}))βπ₯)) = (π Β· ((πΊβπ₯) Β· π
))) |
67 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π¦ β π) β (πΊβπ¦) = (πΊβπ¦)) |
68 | 27, 23, 59, 67 | ofc2 7645 |
. . . . 5
β’ ((π β§ π¦ β π) β ((πΊ βf Β· (π Γ {π
}))βπ¦) = ((πΊβπ¦) Β· π
)) |
69 | 34, 68 | syldan 592 |
. . . 4
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((πΊ βf Β· (π Γ {π
}))βπ¦) = ((πΊβπ¦) Β· π
)) |
70 | 66, 69 | oveq12d 7376 |
. . 3
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((π Β· ((πΊ βf Β· (π Γ {π
}))βπ₯))(+gβπ·)((πΊ βf Β· (π Γ {π
}))βπ¦)) = ((π Β· ((πΊβπ₯) Β· π
))(+gβπ·)((πΊβπ¦) Β· π
))) |
71 | 54, 62, 70 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β ((πΊ βf Β· (π Γ {π
}))β((π( Β·π
βπ)π₯)(+gβπ)π¦)) = ((π Β· ((πΊ βf Β· (π Γ {π
}))βπ₯))(+gβπ·)((πΊ βf Β· (π Γ {π
}))βπ¦))) |
72 | 2, 3, 5, 6, 8, 9, 11, 13, 29, 71, 14 | islfld 37570 |
1
β’ (π β (πΊ βf Β· (π Γ {π
})) β πΉ) |