Step | Hyp | Ref
| Expression |
1 | | eldprdi.w |
. . . . . . 7
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } |
2 | | eldprdi.1 |
. . . . . . 7
β’ (π β πΊdom DProd π) |
3 | | eldprdi.2 |
. . . . . . 7
β’ (π β dom π = πΌ) |
4 | | eldprdi.3 |
. . . . . . 7
β’ (π β πΉ β π) |
5 | | eqid 2732 |
. . . . . . 7
β’
(BaseβπΊ) =
(BaseβπΊ) |
6 | 1, 2, 3, 4, 5 | dprdff 19876 |
. . . . . 6
β’ (π β πΉ:πΌβΆ(BaseβπΊ)) |
7 | 6 | feqmptd 6957 |
. . . . 5
β’ (π β πΉ = (π₯ β πΌ β¦ (πΉβπ₯))) |
8 | 7 | adantr 481 |
. . . 4
β’ ((π β§ (πΊ Ξ£g πΉ) = 0 ) β πΉ = (π₯ β πΌ β¦ (πΉβπ₯))) |
9 | 1, 2, 3, 4 | dprdfcl 19877 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯) β (πβπ₯)) |
10 | 9 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΉβπ₯) β (πβπ₯)) |
11 | | eldprdi.0 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπΊ) |
12 | 2 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΊdom DProd π) |
13 | 3 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β dom π = πΌ) |
14 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β π₯ β πΌ) |
15 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) = (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) |
16 | 11, 1, 12, 13, 14, 10, 15 | dprdfid 19881 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) β π β§ (πΊ Ξ£g (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 ))) = (πΉβπ₯))) |
17 | 16 | simpld 495 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) β π) |
18 | 4 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΉ β π) |
19 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(-gβπΊ) = (-gβπΊ) |
20 | 11, 1, 12, 13, 17, 18, 19 | dprdfsub 19885 |
. . . . . . . . . . 11
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) βf
(-gβπΊ)πΉ) β π β§ (πΊ Ξ£g ((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) βf
(-gβπΊ)πΉ)) = ((πΊ Ξ£g (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0
)))(-gβπΊ)(πΊ Ξ£g πΉ)))) |
21 | 20 | simprd 496 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΊ Ξ£g ((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) βf
(-gβπΊ)πΉ)) = ((πΊ Ξ£g (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0
)))(-gβπΊ)(πΊ Ξ£g πΉ))) |
22 | 2, 3 | dprddomcld 19865 |
. . . . . . . . . . . . 13
β’ (π β πΌ β V) |
23 | 22 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΌ β V) |
24 | | fvex 6901 |
. . . . . . . . . . . . . 14
β’ (πΉβπ₯) β V |
25 | 11 | fvexi 6902 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
26 | 24, 25 | ifex 4577 |
. . . . . . . . . . . . 13
β’ if(π¦ = π₯, (πΉβπ₯), 0 ) β
V |
27 | 26 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β if(π¦ = π₯, (πΉβπ₯), 0 ) β
V) |
28 | | fvexd 6903 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β (πΉβπ¦) β V) |
29 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) = (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 ))) |
30 | 6 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΉ:πΌβΆ(BaseβπΊ)) |
31 | 30 | feqmptd 6957 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΉ = (π¦ β πΌ β¦ (πΉβπ¦))) |
32 | 23, 27, 28, 29, 31 | offval2 7686 |
. . . . . . . . . . 11
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) βf
(-gβπΊ)πΉ) = (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦)))) |
33 | 32 | oveq2d 7421 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΊ Ξ£g ((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) βf
(-gβπΊ)πΉ)) = (πΊ Ξ£g (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))))) |
34 | 16 | simprd 496 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΊ Ξ£g (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 ))) = (πΉβπ₯)) |
35 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΊ Ξ£g πΉ) = 0 ) |
36 | 34, 35 | oveq12d 7423 |
. . . . . . . . . . 11
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((πΊ Ξ£g (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0
)))(-gβπΊ)(πΊ Ξ£g πΉ)) = ((πΉβπ₯)(-gβπΊ) 0 )) |
37 | | dprdgrp 19869 |
. . . . . . . . . . . . 13
β’ (πΊdom DProd π β πΊ β Grp) |
38 | 12, 37 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΊ β Grp) |
39 | 30, 14 | ffvelcdmd 7084 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΉβπ₯) β (BaseβπΊ)) |
40 | 5, 11, 19 | grpsubid1 18904 |
. . . . . . . . . . . 12
β’ ((πΊ β Grp β§ (πΉβπ₯) β (BaseβπΊ)) β ((πΉβπ₯)(-gβπΊ) 0 ) = (πΉβπ₯)) |
41 | 38, 39, 40 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((πΉβπ₯)(-gβπΊ) 0 ) = (πΉβπ₯)) |
42 | 36, 41 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((πΊ Ξ£g (π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0
)))(-gβπΊ)(πΊ Ξ£g πΉ)) = (πΉβπ₯)) |
43 | 21, 33, 42 | 3eqtr3d 2780 |
. . . . . . . . 9
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΊ Ξ£g (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦)))) = (πΉβπ₯)) |
44 | | eqid 2732 |
. . . . . . . . . 10
β’
(CntzβπΊ) =
(CntzβπΊ) |
45 | | grpmnd 18822 |
. . . . . . . . . . . 12
β’ (πΊ β Grp β πΊ β Mnd) |
46 | 2, 37, 45 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β πΊ β Mnd) |
47 | 46 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β πΊ β Mnd) |
48 | 5 | subgacs 19035 |
. . . . . . . . . . . . 13
β’ (πΊ β Grp β
(SubGrpβπΊ) β
(ACSβ(BaseβπΊ))) |
49 | | acsmre 17592 |
. . . . . . . . . . . . 13
β’
((SubGrpβπΊ)
β (ACSβ(BaseβπΊ)) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
50 | 38, 48, 49 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (SubGrpβπΊ) β (Mooreβ(BaseβπΊ))) |
51 | | imassrn 6068 |
. . . . . . . . . . . . . 14
β’ (π β (πΌ β {π₯})) β ran π |
52 | 2, 3 | dprdf2 19871 |
. . . . . . . . . . . . . . . . 17
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
53 | 52 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β π:πΌβΆ(SubGrpβπΊ)) |
54 | 53 | frnd 6722 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ran π β (SubGrpβπΊ)) |
55 | | mresspw 17532 |
. . . . . . . . . . . . . . . 16
β’
((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (SubGrpβπΊ) β π« (BaseβπΊ)) |
57 | 54, 56 | sstrd 3991 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ran π β π« (BaseβπΊ)) |
58 | 51, 57 | sstrid 3992 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (π β (πΌ β {π₯})) β π« (BaseβπΊ)) |
59 | | sspwuni 5102 |
. . . . . . . . . . . . 13
β’ ((π β (πΌ β {π₯})) β π« (BaseβπΊ) β βͺ (π
β (πΌ β {π₯})) β (BaseβπΊ)) |
60 | 58, 59 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β βͺ (π β (πΌ β {π₯})) β (BaseβπΊ)) |
61 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(mrClsβ(SubGrpβπΊ)) = (mrClsβ(SubGrpβπΊ)) |
62 | 61 | mrccl 17551 |
. . . . . . . . . . . 12
β’
(((SubGrpβπΊ)
β (Mooreβ(BaseβπΊ)) β§ βͺ (π β (πΌ β {π₯})) β (BaseβπΊ)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (SubGrpβπΊ)) |
63 | 50, 60, 62 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (SubGrpβπΊ)) |
64 | | subgsubm 19022 |
. . . . . . . . . . 11
β’
(((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯}))) β (SubGrpβπΊ) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (SubMndβπΊ)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (SubMndβπΊ)) |
66 | | oveq1 7412 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) = if(π¦ = π₯, (πΉβπ₯), 0 ) β ((πΉβπ₯)(-gβπΊ)(πΉβπ¦)) = (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))) |
67 | 66 | eleq1d 2818 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) = if(π¦ = π₯, (πΉβπ₯), 0 ) β (((πΉβπ₯)(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
68 | | oveq1 7412 |
. . . . . . . . . . . . 13
β’ ( 0 = if(π¦ = π₯, (πΉβπ₯), 0 ) β ( 0
(-gβπΊ)(πΉβπ¦)) = (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))) |
69 | 68 | eleq1d 2818 |
. . . . . . . . . . . 12
β’ ( 0 = if(π¦ = π₯, (πΉβπ₯), 0 ) β (( 0
(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
70 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ π¦ = π₯) β π¦ = π₯) |
71 | 70 | fveq2d 6892 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ π¦ = π₯) β (πΉβπ¦) = (πΉβπ₯)) |
72 | 71 | oveq2d 7421 |
. . . . . . . . . . . . 13
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ π¦ = π₯) β ((πΉβπ₯)(-gβπΊ)(πΉβπ¦)) = ((πΉβπ₯)(-gβπΊ)(πΉβπ₯))) |
73 | 5, 11, 19 | grpsubid 18903 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β Grp β§ (πΉβπ₯) β (BaseβπΊ)) β ((πΉβπ₯)(-gβπΊ)(πΉβπ₯)) = 0 ) |
74 | 38, 39, 73 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((πΉβπ₯)(-gβπΊ)(πΉβπ₯)) = 0 ) |
75 | 11 | subg0cl 19008 |
. . . . . . . . . . . . . . . 16
β’
(((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯}))) β (SubGrpβπΊ) β 0 β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯})))) |
76 | 63, 75 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β 0 β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯})))) |
77 | 74, 76 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((πΉβπ₯)(-gβπΊ)(πΉβπ₯)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
78 | 77 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ π¦ = π₯) β ((πΉβπ₯)(-gβπΊ)(πΉβπ₯)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
79 | 72, 78 | eqeltrd 2833 |
. . . . . . . . . . . 12
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ π¦ = π₯) β ((πΉβπ₯)(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
80 | 63 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))) β (SubGrpβπΊ)) |
81 | 80, 75 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β 0 β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯})))) |
82 | 50, 61, 60 | mrcssidd 17565 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β βͺ (π β (πΌ β {π₯})) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
83 | 82 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β βͺ (π β (πΌ β {π₯})) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
84 | 1, 12, 13, 18 | dprdfcl 19877 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β (πΉβπ¦) β (πβπ¦)) |
85 | 84 | adantr 481 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β (πΉβπ¦) β (πβπ¦)) |
86 | 53 | ffnd 6715 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β π Fn πΌ) |
87 | 86 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β π Fn πΌ) |
88 | | difssd 4131 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β (πΌ β {π₯}) β πΌ) |
89 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π₯ β Β¬ π¦ = π₯) |
90 | | eldifsn 4789 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (πΌ β {π₯}) β (π¦ β πΌ β§ π¦ β π₯)) |
91 | 90 | biimpri 227 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β πΌ β§ π¦ β π₯) β π¦ β (πΌ β {π₯})) |
92 | 89, 91 | sylan2br 595 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β πΌ β§ Β¬ π¦ = π₯) β π¦ β (πΌ β {π₯})) |
93 | 92 | adantll 712 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β π¦ β (πΌ β {π₯})) |
94 | | fnfvima 7231 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn πΌ β§ (πΌ β {π₯}) β πΌ β§ π¦ β (πΌ β {π₯})) β (πβπ¦) β (π β (πΌ β {π₯}))) |
95 | 87, 88, 93, 94 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β (πβπ¦) β (π β (πΌ β {π₯}))) |
96 | | elunii 4912 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ¦) β (πβπ¦) β§ (πβπ¦) β (π β (πΌ β {π₯}))) β (πΉβπ¦) β βͺ (π β (πΌ β {π₯}))) |
97 | 85, 95, 96 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β (πΉβπ¦) β βͺ (π β (πΌ β {π₯}))) |
98 | 83, 97 | sseldd 3982 |
. . . . . . . . . . . . 13
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β (πΉβπ¦) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
99 | 19 | subgsubcl 19011 |
. . . . . . . . . . . . 13
β’
((((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯}))) β (SubGrpβπΊ) β§ 0 β
((mrClsβ(SubGrpβπΊ))ββͺ (π β (πΌ β {π₯}))) β§ (πΉβπ¦) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) β ( 0
(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
100 | 80, 81, 98, 99 | syl3anc 1371 |
. . . . . . . . . . . 12
β’
(((((π β§ (πΊ Ξ£g
πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β§ Β¬ π¦ = π₯) β ( 0 (-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
101 | 67, 69, 79, 100 | ifbothda 4565 |
. . . . . . . . . . 11
β’ ((((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β§ π¦ β πΌ) β (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦)) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
102 | 101 | fmpttd 7111 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))):πΌβΆ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
103 | 20 | simpld 495 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((π¦ β πΌ β¦ if(π¦ = π₯, (πΉβπ₯), 0 )) βf
(-gβπΊ)πΉ) β π) |
104 | 32, 103 | eqeltrrd 2834 |
. . . . . . . . . . 11
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))) β π) |
105 | 1, 12, 13, 104, 44 | dprdfcntz 19879 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ran (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))) β ((CntzβπΊ)βran (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))))) |
106 | 1, 12, 13, 104 | dprdffsupp 19878 |
. . . . . . . . . 10
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦))) finSupp 0 ) |
107 | 11, 44, 47, 23, 65, 102, 105, 106 | gsumzsubmcl 19780 |
. . . . . . . . 9
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΊ Ξ£g (π¦ β πΌ β¦ (if(π¦ = π₯, (πΉβπ₯), 0
)(-gβπΊ)(πΉβπ¦)))) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
108 | 43, 107 | eqeltrrd 2834 |
. . . . . . . 8
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΉβπ₯) β ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) |
109 | 10, 108 | elind 4193 |
. . . . . . 7
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΉβπ₯) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯}))))) |
110 | 12, 13, 14, 11, 61 | dprddisj 19873 |
. . . . . . 7
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β ((πβπ₯) β© ((mrClsβ(SubGrpβπΊ))ββͺ (π
β (πΌ β {π₯})))) = { 0 }) |
111 | 109, 110 | eleqtrd 2835 |
. . . . . 6
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΉβπ₯) β { 0 }) |
112 | | elsni 4644 |
. . . . . 6
β’ ((πΉβπ₯) β { 0 } β (πΉβπ₯) = 0 ) |
113 | 111, 112 | syl 17 |
. . . . 5
β’ (((π β§ (πΊ Ξ£g πΉ) = 0 ) β§ π₯ β πΌ) β (πΉβπ₯) = 0 ) |
114 | 113 | mpteq2dva 5247 |
. . . 4
β’ ((π β§ (πΊ Ξ£g πΉ) = 0 ) β (π₯ β πΌ β¦ (πΉβπ₯)) = (π₯ β πΌ β¦ 0 )) |
115 | 8, 114 | eqtrd 2772 |
. . 3
β’ ((π β§ (πΊ Ξ£g πΉ) = 0 ) β πΉ = (π₯ β πΌ β¦ 0 )) |
116 | 115 | ex 413 |
. 2
β’ (π β ((πΊ Ξ£g πΉ) = 0 β πΉ = (π₯ β πΌ β¦ 0 ))) |
117 | 11 | gsumz 18713 |
. . . 4
β’ ((πΊ β Mnd β§ πΌ β V) β (πΊ Ξ£g
(π₯ β πΌ β¦ 0 )) = 0 ) |
118 | 46, 22, 117 | syl2anc 584 |
. . 3
β’ (π β (πΊ Ξ£g (π₯ β πΌ β¦ 0 )) = 0 ) |
119 | | oveq2 7413 |
. . . 4
β’ (πΉ = (π₯ β πΌ β¦ 0 ) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (π₯ β πΌ β¦ 0 ))) |
120 | 119 | eqeq1d 2734 |
. . 3
β’ (πΉ = (π₯ β πΌ β¦ 0 ) β ((πΊ Ξ£g
πΉ) = 0 β (πΊ Ξ£g (π₯ β πΌ β¦ 0 )) = 0 )) |
121 | 118, 120 | syl5ibrcom 246 |
. 2
β’ (π β (πΉ = (π₯ β πΌ β¦ 0 ) β (πΊ Ξ£g
πΉ) = 0 )) |
122 | 116, 121 | impbid 211 |
1
β’ (π β ((πΊ Ξ£g πΉ) = 0 β πΉ = (π₯ β πΌ β¦ 0 ))) |