Step | Hyp | Ref
| Expression |
1 | | frlmphl.y |
. . . 4
β’ π = (π
freeLMod πΌ) |
2 | | eqid 2737 |
. . . . . . 7
β’ (π
freeLMod πΌ) = (π
freeLMod πΌ) |
3 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(π
freeLMod πΌ)) =
(Baseβ(π
freeLMod
πΌ)) |
4 | 2, 3 | frlmpws 21109 |
. . . . . 6
β’ ((π
β π β§ πΌ β π) β (π
freeLMod πΌ) = (((ringLModβπ
) βs πΌ) βΎs
(Baseβ(π
freeLMod
πΌ)))) |
5 | 4 | ancoms 459 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β (π
freeLMod πΌ) = (((ringLModβπ
) βs πΌ) βΎs
(Baseβ(π
freeLMod
πΌ)))) |
6 | | frlmphl.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ
) |
7 | 6 | ressid 17085 |
. . . . . . . . . 10
β’ (π
β π β (π
βΎs π΅) = π
) |
8 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π
β π β ((subringAlg βπ
)βπ΅) = ((subringAlg βπ
)βπ΅)) |
9 | 6 | eqimssi 4000 |
. . . . . . . . . . . 12
β’ π΅ β (Baseβπ
) |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
β’ (π
β π β π΅ β (Baseβπ
)) |
11 | 8, 10 | srasca 20599 |
. . . . . . . . . 10
β’ (π
β π β (π
βΎs π΅) = (Scalarβ((subringAlg βπ
)βπ΅))) |
12 | 7, 11 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π
β π β π
= (Scalarβ((subringAlg βπ
)βπ΅))) |
13 | 12 | oveq1d 7366 |
. . . . . . . 8
β’ (π
β π β (π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) = ((Scalarβ((subringAlg
βπ
)βπ΅))Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
14 | 13 | adantl 482 |
. . . . . . 7
β’ ((πΌ β π β§ π
β π) β (π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) = ((Scalarβ((subringAlg
βπ
)βπ΅))Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
15 | | fvex 6852 |
. . . . . . . . 9
β’
((subringAlg βπ
)βπ΅) β V |
16 | | rlmval 20613 |
. . . . . . . . . . . 12
β’
(ringLModβπ
) =
((subringAlg βπ
)β(Baseβπ
)) |
17 | 6 | fveq2i 6842 |
. . . . . . . . . . . 12
β’
((subringAlg βπ
)βπ΅) = ((subringAlg βπ
)β(Baseβπ
)) |
18 | 16, 17 | eqtr4i 2768 |
. . . . . . . . . . 11
β’
(ringLModβπ
) =
((subringAlg βπ
)βπ΅) |
19 | 18 | oveq1i 7361 |
. . . . . . . . . 10
β’
((ringLModβπ
)
βs πΌ) = (((subringAlg βπ
)βπ΅) βs πΌ) |
20 | | eqid 2737 |
. . . . . . . . . 10
β’
(Scalarβ((subringAlg βπ
)βπ΅)) = (Scalarβ((subringAlg βπ
)βπ΅)) |
21 | 19, 20 | pwsval 17328 |
. . . . . . . . 9
β’
((((subringAlg βπ
)βπ΅) β V β§ πΌ β π) β ((ringLModβπ
) βs πΌ) = ((Scalarβ((subringAlg
βπ
)βπ΅))Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
22 | 15, 21 | mpan 688 |
. . . . . . . 8
β’ (πΌ β π β ((ringLModβπ
) βs πΌ) = ((Scalarβ((subringAlg
βπ
)βπ΅))Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
23 | 22 | adantr 481 |
. . . . . . 7
β’ ((πΌ β π β§ π
β π) β ((ringLModβπ
) βs πΌ) = ((Scalarβ((subringAlg
βπ
)βπ΅))Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
24 | 14, 23 | eqtr4d 2780 |
. . . . . 6
β’ ((πΌ β π β§ π
β π) β (π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) = ((ringLModβπ
) βs πΌ)) |
25 | 1 | fveq2i 6842 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβ(π
freeLMod
πΌ)) |
26 | 25 | a1i 11 |
. . . . . 6
β’ ((πΌ β π β§ π
β π) β (Baseβπ) = (Baseβ(π
freeLMod πΌ))) |
27 | 24, 26 | oveq12d 7369 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ)) = (((ringLModβπ
) βs
πΌ) βΎs
(Baseβ(π
freeLMod
πΌ)))) |
28 | 5, 27 | eqtr4d 2780 |
. . . 4
β’ ((πΌ β π β§ π
β π) β (π
freeLMod πΌ) = ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ))) |
29 | 1, 28 | eqtrid 2789 |
. . 3
β’ ((πΌ β π β§ π
β π) β π = ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ))) |
30 | 29 | fveq2d 6843 |
. 2
β’ ((πΌ β π β§ π
β π) β
(Β·πβπ) =
(Β·πβ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ)))) |
31 | | fvex 6852 |
. . . 4
β’
(Baseβπ)
β V |
32 | | eqid 2737 |
. . . . 5
β’ ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ)) = ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ)) |
33 | | eqid 2737 |
. . . . 5
β’
(Β·πβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) =
(Β·πβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
34 | 32, 33 | ressip 17186 |
. . . 4
β’
((Baseβπ)
β V β (Β·πβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) =
(Β·πβ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ)))) |
35 | 31, 34 | ax-mp 5 |
. . 3
β’
(Β·πβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) =
(Β·πβ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ))) |
36 | | eqid 2737 |
. . . . 5
β’ (π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) = (π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) |
37 | | simpr 485 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β π
β π) |
38 | | snex 5386 |
. . . . . . 7
β’
{((subringAlg βπ
)βπ΅)} β V |
39 | | xpexg 7676 |
. . . . . . 7
β’ ((πΌ β π β§ {((subringAlg βπ
)βπ΅)} β V) β (πΌ Γ {((subringAlg βπ
)βπ΅)}) β V) |
40 | 38, 39 | mpan2 689 |
. . . . . 6
β’ (πΌ β π β (πΌ Γ {((subringAlg βπ
)βπ΅)}) β V) |
41 | 40 | adantr 481 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β (πΌ Γ {((subringAlg βπ
)βπ΅)}) β V) |
42 | | eqid 2737 |
. . . . 5
β’
(Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) = (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) |
43 | 15 | snnz 4735 |
. . . . . 6
β’
{((subringAlg βπ
)βπ΅)} β β
|
44 | | dmxp 5882 |
. . . . . 6
β’
({((subringAlg βπ
)βπ΅)} β β
β dom (πΌ Γ {((subringAlg
βπ
)βπ΅)}) = πΌ) |
45 | 43, 44 | mp1i 13 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β dom (πΌ Γ {((subringAlg βπ
)βπ΅)}) = πΌ) |
46 | 36, 37, 41, 42, 45, 33 | prdsip 17303 |
. . . 4
β’ ((πΌ β π β§ π
β π) β
(Β·πβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) = (π β (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))), π β (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) β¦ (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))(πβπ₯)))))) |
47 | 36, 37, 41, 42, 45 | prdsbas 17299 |
. . . . . 6
β’ ((πΌ β π β§ π
β π) β (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) = Xπ₯ β πΌ (Baseβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))) |
48 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π₯ β πΌ β ((subringAlg βπ
)βπ΅) = ((subringAlg βπ
)βπ΅)) |
49 | 9 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β πΌ β π΅ β (Baseβπ
)) |
50 | 48, 49 | srabase 20593 |
. . . . . . . . 9
β’ (π₯ β πΌ β (Baseβπ
) = (Baseβ((subringAlg βπ
)βπ΅))) |
51 | 6 | a1i 11 |
. . . . . . . . 9
β’ (π₯ β πΌ β π΅ = (Baseβπ
)) |
52 | 15 | fvconst2 7149 |
. . . . . . . . . 10
β’ (π₯ β πΌ β ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯) = ((subringAlg βπ
)βπ΅)) |
53 | 52 | fveq2d 6843 |
. . . . . . . . 9
β’ (π₯ β πΌ β (Baseβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯)) = (Baseβ((subringAlg βπ
)βπ΅))) |
54 | 50, 51, 53 | 3eqtr4rd 2788 |
. . . . . . . 8
β’ (π₯ β πΌ β (Baseβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯)) = π΅) |
55 | 54 | adantl 482 |
. . . . . . 7
β’ (((πΌ β π β§ π
β π) β§ π₯ β πΌ) β (Baseβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯)) = π΅) |
56 | 55 | ixpeq2dva 8808 |
. . . . . 6
β’ ((πΌ β π β§ π
β π) β Xπ₯ β πΌ (Baseβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯)) = Xπ₯ β πΌ π΅) |
57 | 6 | fvexi 6853 |
. . . . . . . 8
β’ π΅ β V |
58 | | ixpconstg 8802 |
. . . . . . . 8
β’ ((πΌ β π β§ π΅ β V) β Xπ₯ β
πΌ π΅ = (π΅ βm πΌ)) |
59 | 57, 58 | mpan2 689 |
. . . . . . 7
β’ (πΌ β π β Xπ₯ β πΌ π΅ = (π΅ βm πΌ)) |
60 | 59 | adantr 481 |
. . . . . 6
β’ ((πΌ β π β§ π
β π) β Xπ₯ β πΌ π΅ = (π΅ βm πΌ)) |
61 | 47, 56, 60 | 3eqtrd 2781 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) = (π΅ βm πΌ)) |
62 | | frlmphl.t |
. . . . . . . . . 10
β’ Β· =
(.rβπ
) |
63 | 52, 49 | sraip 20603 |
. . . . . . . . . 10
β’ (π₯ β πΌ β (.rβπ
) =
(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))) |
64 | 62, 63 | eqtr2id 2790 |
. . . . . . . . 9
β’ (π₯ β πΌ β
(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯)) = Β· ) |
65 | 64 | oveqd 7368 |
. . . . . . . 8
β’ (π₯ β πΌ β ((πβπ₯)(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))(πβπ₯)) = ((πβπ₯) Β· (πβπ₯))) |
66 | 65 | mpteq2ia 5206 |
. . . . . . 7
β’ (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))(πβπ₯))) = (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯))) |
67 | 66 | oveq2i 7362 |
. . . . . 6
β’ (π
Ξ£g
(π₯ β πΌ β¦ ((πβπ₯)(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))(πβπ₯)))) = (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯)))) |
68 | 67 | a1i 11 |
. . . . 5
β’ ((πΌ β π β§ π
β π) β (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))(πβπ₯)))) = (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯))))) |
69 | 61, 61, 68 | mpoeq123dv 7426 |
. . . 4
β’ ((πΌ β π β§ π
β π) β (π β (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))), π β (Baseβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) β¦ (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ((πΌ Γ {((subringAlg βπ
)βπ΅)})βπ₯))(πβπ₯))))) = (π β (π΅ βm πΌ), π β (π΅ βm πΌ) β¦ (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯)))))) |
70 | 46, 69 | eqtrd 2777 |
. . 3
β’ ((πΌ β π β§ π
β π) β
(Β·πβ(π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)}))) = (π β (π΅ βm πΌ), π β (π΅ βm πΌ) β¦ (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯)))))) |
71 | 35, 70 | eqtr3id 2791 |
. 2
β’ ((πΌ β π β§ π
β π) β
(Β·πβ((π
Xs(πΌ Γ {((subringAlg βπ
)βπ΅)})) βΎs (Baseβπ))) = (π β (π΅ βm πΌ), π β (π΅ βm πΌ) β¦ (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯)))))) |
72 | 30, 71 | eqtr2d 2778 |
1
β’ ((πΌ β π β§ π
β π) β (π β (π΅ βm πΌ), π β (π΅ βm πΌ) β¦ (π
Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯))))) =
(Β·πβπ)) |