Step | Hyp | Ref
| Expression |
1 | | iccssxr 13276 |
. . . . . . 7
β’
(0[,]+β) β β* |
2 | | xrge0gsumle.g |
. . . . . . . . . 10
β’ πΊ =
(β*π βΎs
(0[,]+β)) |
3 | | xrsbas 20736 |
. . . . . . . . . 10
β’
β* =
(Baseββ*π ) |
4 | 2, 3 | ressbas2 17055 |
. . . . . . . . 9
β’
((0[,]+β) β β* β (0[,]+β) =
(BaseβπΊ)) |
5 | 1, 4 | ax-mp 5 |
. . . . . . . 8
β’
(0[,]+β) = (BaseβπΊ) |
6 | | eqid 2738 |
. . . . . . . . . 10
β’
(β*π βΎs
(β* β {-β})) =
(β*π βΎs
(β* β {-β})) |
7 | 6 | xrge0subm 20761 |
. . . . . . . . 9
β’
(0[,]+β) β
(SubMndβ(β*π βΎs
(β* β {-β}))) |
8 | | xrex 12841 |
. . . . . . . . . . . . 13
β’
β* β V |
9 | 8 | difexi 5284 |
. . . . . . . . . . . 12
β’
(β* β {-β}) β V |
10 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ 0 β€ π₯) β
π₯ β
β*) |
11 | | ge0nemnf 13021 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ 0 β€ π₯) β
π₯ β
-β) |
12 | 10, 11 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β*
β§ 0 β€ π₯) β
(π₯ β
β* β§ π₯
β -β)) |
13 | | elxrge0 13303 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0[,]+β) β
(π₯ β
β* β§ 0 β€ π₯)) |
14 | | eldifsn 4746 |
. . . . . . . . . . . . . 14
β’ (π₯ β (β*
β {-β}) β (π₯ β β* β§ π₯ β
-β)) |
15 | 12, 13, 14 | 3imtr4i 292 |
. . . . . . . . . . . . 13
β’ (π₯ β (0[,]+β) β
π₯ β
(β* β {-β})) |
16 | 15 | ssriv 3947 |
. . . . . . . . . . . 12
β’
(0[,]+β) β (β* β
{-β}) |
17 | | ressabs 17065 |
. . . . . . . . . . . 12
β’
(((β* β {-β}) β V β§ (0[,]+β)
β (β* β {-β})) β
((β*π βΎs
(β* β {-β})) βΎs (0[,]+β)) =
(β*π βΎs
(0[,]+β))) |
18 | 9, 16, 17 | mp2an 691 |
. . . . . . . . . . 11
β’
((β*π βΎs
(β* β {-β})) βΎs (0[,]+β)) =
(β*π βΎs
(0[,]+β)) |
19 | 2, 18 | eqtr4i 2769 |
. . . . . . . . . 10
β’ πΊ =
((β*π βΎs
(β* β {-β})) βΎs
(0[,]+β)) |
20 | 6 | xrs10 20759 |
. . . . . . . . . 10
β’ 0 =
(0gβ(β*π
βΎs (β* β {-β}))) |
21 | 19, 20 | subm0 18561 |
. . . . . . . . 9
β’
((0[,]+β) β
(SubMndβ(β*π βΎs
(β* β {-β}))) β 0 =
(0gβπΊ)) |
22 | 7, 21 | ax-mp 5 |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
23 | | xrge0cmn 20762 |
. . . . . . . . . 10
β’
(β*π βΎs
(0[,]+β)) β CMnd |
24 | 2, 23 | eqeltri 2835 |
. . . . . . . . 9
β’ πΊ β CMnd |
25 | 24 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (π« π΄ β© Fin)) β πΊ β CMnd) |
26 | | elfpw 9232 |
. . . . . . . . . 10
β’ (π β (π« π΄ β© Fin) β (π β π΄ β§ π β Fin)) |
27 | 26 | simprbi 498 |
. . . . . . . . 9
β’ (π β (π« π΄ β© Fin) β π β Fin) |
28 | 27 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (π« π΄ β© Fin)) β π β Fin) |
29 | | xrge0gsumle.f |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆ(0[,]+β)) |
30 | 26 | simplbi 499 |
. . . . . . . . 9
β’ (π β (π« π΄ β© Fin) β π β π΄) |
31 | | fssres 6704 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆ(0[,]+β) β§ π β π΄) β (πΉ βΎ π ):π βΆ(0[,]+β)) |
32 | 29, 30, 31 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΉ βΎ π ):π βΆ(0[,]+β)) |
33 | | c0ex 11083 |
. . . . . . . . . 10
β’ 0 β
V |
34 | 33 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (π« π΄ β© Fin)) β 0 β
V) |
35 | 32, 28, 34 | fdmfifsupp 9249 |
. . . . . . . 8
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΉ βΎ π ) finSupp 0) |
36 | 5, 22, 25, 28, 32, 35 | gsumcl 19621 |
. . . . . . 7
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π )) β (0[,]+β)) |
37 | 1, 36 | sselid 3941 |
. . . . . 6
β’ ((π β§ π β (π« π΄ β© Fin)) β (πΊ Ξ£g (πΉ βΎ π )) β
β*) |
38 | 37 | fmpttd 7058 |
. . . . 5
β’ (π β (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))):(π« π΄ β©
Fin)βΆβ*) |
39 | 38 | frnd 6672 |
. . . 4
β’ (π β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))) β
β*) |
40 | | 0ss 4355 |
. . . . . . 7
β’ β
β π΄ |
41 | | 0fin 9049 |
. . . . . . 7
β’ β
β Fin |
42 | | elfpw 9232 |
. . . . . . 7
β’ (β
β (π« π΄ β©
Fin) β (β
β π΄ β§ β
β Fin)) |
43 | 40, 41, 42 | mpbir2an 710 |
. . . . . 6
β’ β
β (π« π΄ β©
Fin) |
44 | | 0cn 11081 |
. . . . . 6
β’ 0 β
β |
45 | | eqid 2738 |
. . . . . . 7
β’ (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) = (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))) |
46 | | reseq2 5929 |
. . . . . . . . . 10
β’ (π = β
β (πΉ βΎ π ) = (πΉ βΎ β
)) |
47 | | res0 5938 |
. . . . . . . . . 10
β’ (πΉ βΎ β
) =
β
|
48 | 46, 47 | eqtrdi 2794 |
. . . . . . . . 9
β’ (π = β
β (πΉ βΎ π ) = β
) |
49 | 48 | oveq2d 7366 |
. . . . . . . 8
β’ (π = β
β (πΊ Ξ£g
(πΉ βΎ π )) = (πΊ Ξ£g
β
)) |
50 | 22 | gsum0 18474 |
. . . . . . . 8
β’ (πΊ Ξ£g
β
) = 0 |
51 | 49, 50 | eqtrdi 2794 |
. . . . . . 7
β’ (π = β
β (πΊ Ξ£g
(πΉ βΎ π )) = 0) |
52 | 45, 51 | elrnmpt1s 5909 |
. . . . . 6
β’ ((β
β (π« π΄ β©
Fin) β§ 0 β β) β 0 β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π )))) |
53 | 43, 44, 52 | mp2an 691 |
. . . . 5
β’ 0 β
ran (π β (π«
π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π ))) |
54 | 53 | a1i 11 |
. . . 4
β’ (π β 0 β ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g
(πΉ βΎ π )))) |
55 | 39, 54 | sseldd 3944 |
. . 3
β’ (π β 0 β
β*) |
56 | 24 | a1i 11 |
. . . . 5
β’ (π β πΊ β CMnd) |
57 | | xrge0gsumle.b |
. . . . . . 7
β’ (π β π΅ β (π« π΄ β© Fin)) |
58 | 57 | elin2d 4158 |
. . . . . 6
β’ (π β π΅ β Fin) |
59 | | diffi 9057 |
. . . . . 6
β’ (π΅ β Fin β (π΅ β πΆ) β Fin) |
60 | 58, 59 | syl 17 |
. . . . 5
β’ (π β (π΅ β πΆ) β Fin) |
61 | | elfpw 9232 |
. . . . . . . . 9
β’ (π΅ β (π« π΄ β© Fin) β (π΅ β π΄ β§ π΅ β Fin)) |
62 | 61 | simplbi 499 |
. . . . . . . 8
β’ (π΅ β (π« π΄ β© Fin) β π΅ β π΄) |
63 | 57, 62 | syl 17 |
. . . . . . 7
β’ (π β π΅ β π΄) |
64 | 63 | ssdifssd 4101 |
. . . . . 6
β’ (π β (π΅ β πΆ) β π΄) |
65 | 29, 64 | fssresd 6705 |
. . . . 5
β’ (π β (πΉ βΎ (π΅ β πΆ)):(π΅ β πΆ)βΆ(0[,]+β)) |
66 | 33 | a1i 11 |
. . . . . 6
β’ (π β 0 β
V) |
67 | 65, 60, 66 | fdmfifsupp 9249 |
. . . . 5
β’ (π β (πΉ βΎ (π΅ β πΆ)) finSupp 0) |
68 | 5, 22, 56, 60, 65, 67 | gsumcl 19621 |
. . . 4
β’ (π β (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ))) β (0[,]+β)) |
69 | 1, 68 | sselid 3941 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ))) β
β*) |
70 | | xrge0gsumle.c |
. . . . . 6
β’ (π β πΆ β π΅) |
71 | 58, 70 | ssfid 9145 |
. . . . 5
β’ (π β πΆ β Fin) |
72 | 70, 63 | sstrd 3953 |
. . . . . 6
β’ (π β πΆ β π΄) |
73 | 29, 72 | fssresd 6705 |
. . . . 5
β’ (π β (πΉ βΎ πΆ):πΆβΆ(0[,]+β)) |
74 | 73, 71, 66 | fdmfifsupp 9249 |
. . . . 5
β’ (π β (πΉ βΎ πΆ) finSupp 0) |
75 | 5, 22, 56, 71, 73, 74 | gsumcl 19621 |
. . . 4
β’ (π β (πΊ Ξ£g (πΉ βΎ πΆ)) β (0[,]+β)) |
76 | 1, 75 | sselid 3941 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ πΆ)) β
β*) |
77 | | elxrge0 13303 |
. . . . 5
β’ ((πΊ Ξ£g
(πΉ βΎ (π΅ β πΆ))) β (0[,]+β) β ((πΊ Ξ£g
(πΉ βΎ (π΅ β πΆ))) β β* β§ 0 β€
(πΊ
Ξ£g (πΉ βΎ (π΅ β πΆ))))) |
78 | 77 | simprbi 498 |
. . . 4
β’ ((πΊ Ξ£g
(πΉ βΎ (π΅ β πΆ))) β (0[,]+β) β 0 β€
(πΊ
Ξ£g (πΉ βΎ (π΅ β πΆ)))) |
79 | 68, 78 | syl 17 |
. . 3
β’ (π β 0 β€ (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ)))) |
80 | | xleadd2a 13102 |
. . 3
β’ (((0
β β* β§ (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ))) β β* β§ (πΊ Ξ£g
(πΉ βΎ πΆ)) β β*)
β§ 0 β€ (πΊ
Ξ£g (πΉ βΎ (π΅ β πΆ)))) β ((πΊ Ξ£g (πΉ βΎ πΆ)) +π 0) β€ ((πΊ Ξ£g
(πΉ βΎ πΆ)) +π (πΊ Ξ£g
(πΉ βΎ (π΅ β πΆ))))) |
81 | 55, 69, 76, 79, 80 | syl31anc 1374 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ πΆ)) +π 0) β€ ((πΊ Ξ£g
(πΉ βΎ πΆ)) +π (πΊ Ξ£g
(πΉ βΎ (π΅ β πΆ))))) |
82 | 76 | xaddid1d 13091 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ πΆ)) +π 0) = (πΊ Ξ£g
(πΉ βΎ πΆ))) |
83 | | ovex 7383 |
. . . . 5
β’
(0[,]+β) β V |
84 | | xrsadd 20737 |
. . . . . 6
β’
+π =
(+gββ*π ) |
85 | 2, 84 | ressplusg 17106 |
. . . . 5
β’
((0[,]+β) β V β +π =
(+gβπΊ)) |
86 | 83, 85 | ax-mp 5 |
. . . 4
β’
+π = (+gβπΊ) |
87 | 29, 63 | fssresd 6705 |
. . . 4
β’ (π β (πΉ βΎ π΅):π΅βΆ(0[,]+β)) |
88 | 87, 58, 66 | fdmfifsupp 9249 |
. . . 4
β’ (π β (πΉ βΎ π΅) finSupp 0) |
89 | | disjdif 4430 |
. . . . 5
β’ (πΆ β© (π΅ β πΆ)) = β
|
90 | 89 | a1i 11 |
. . . 4
β’ (π β (πΆ β© (π΅ β πΆ)) = β
) |
91 | | undif2 4435 |
. . . . 5
β’ (πΆ βͺ (π΅ β πΆ)) = (πΆ βͺ π΅) |
92 | | ssequn1 4139 |
. . . . . 6
β’ (πΆ β π΅ β (πΆ βͺ π΅) = π΅) |
93 | 70, 92 | sylib 217 |
. . . . 5
β’ (π β (πΆ βͺ π΅) = π΅) |
94 | 91, 93 | eqtr2id 2791 |
. . . 4
β’ (π β π΅ = (πΆ βͺ (π΅ β πΆ))) |
95 | 5, 22, 86, 56, 57, 87, 88, 90, 94 | gsumsplit 19634 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ π΅)) = ((πΊ Ξ£g ((πΉ βΎ π΅) βΎ πΆ)) +π (πΊ Ξ£g ((πΉ βΎ π΅) βΎ (π΅ β πΆ))))) |
96 | 70 | resabs1d 5965 |
. . . . 5
β’ (π β ((πΉ βΎ π΅) βΎ πΆ) = (πΉ βΎ πΆ)) |
97 | 96 | oveq2d 7366 |
. . . 4
β’ (π β (πΊ Ξ£g ((πΉ βΎ π΅) βΎ πΆ)) = (πΊ Ξ£g (πΉ βΎ πΆ))) |
98 | | difss 4090 |
. . . . . 6
β’ (π΅ β πΆ) β π΅ |
99 | | resabs1 5964 |
. . . . . 6
β’ ((π΅ β πΆ) β π΅ β ((πΉ βΎ π΅) βΎ (π΅ β πΆ)) = (πΉ βΎ (π΅ β πΆ))) |
100 | 98, 99 | mp1i 13 |
. . . . 5
β’ (π β ((πΉ βΎ π΅) βΎ (π΅ β πΆ)) = (πΉ βΎ (π΅ β πΆ))) |
101 | 100 | oveq2d 7366 |
. . . 4
β’ (π β (πΊ Ξ£g ((πΉ βΎ π΅) βΎ (π΅ β πΆ))) = (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ)))) |
102 | 97, 101 | oveq12d 7368 |
. . 3
β’ (π β ((πΊ Ξ£g ((πΉ βΎ π΅) βΎ πΆ)) +π (πΊ Ξ£g ((πΉ βΎ π΅) βΎ (π΅ β πΆ)))) = ((πΊ Ξ£g (πΉ βΎ πΆ)) +π (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ))))) |
103 | 95, 102 | eqtr2d 2779 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ πΆ)) +π (πΊ Ξ£g (πΉ βΎ (π΅ β πΆ)))) = (πΊ Ξ£g (πΉ βΎ π΅))) |
104 | 81, 82, 103 | 3brtr3d 5135 |
1
β’ (π β (πΊ Ξ£g (πΉ βΎ πΆ)) β€ (πΊ Ξ£g (πΉ βΎ π΅))) |