Step | Hyp | Ref
| Expression |
1 | | dsmmcl.p |
. . 3
β’ π = (πXsπ
) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
3 | | dsmmacl.a |
. . 3
β’ + =
(+gβπ) |
4 | | dsmmcl.s |
. . 3
β’ (π β π β π) |
5 | | dsmmcl.i |
. . 3
β’ (π β πΌ β π) |
6 | | dsmmcl.r |
. . 3
β’ (π β π
:πΌβΆMnd) |
7 | | dsmmacl.j |
. . . . 5
β’ (π β π½ β π») |
8 | | eqid 2733 |
. . . . . 6
β’ (π βm π
) = (π βm π
) |
9 | | dsmmcl.h |
. . . . . 6
β’ π» = (Baseβ(π βm π
)) |
10 | 6 | ffnd 6670 |
. . . . . 6
β’ (π β π
Fn πΌ) |
11 | 1, 8, 2, 9, 5, 10 | dsmmelbas 21161 |
. . . . 5
β’ (π β (π½ β π» β (π½ β (Baseβπ) β§ {π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin))) |
12 | 7, 11 | mpbid 231 |
. . . 4
β’ (π β (π½ β (Baseβπ) β§ {π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin)) |
13 | 12 | simpld 496 |
. . 3
β’ (π β π½ β (Baseβπ)) |
14 | | dsmmacl.k |
. . . . 5
β’ (π β πΎ β π») |
15 | 1, 8, 2, 9, 5, 10 | dsmmelbas 21161 |
. . . . 5
β’ (π β (πΎ β π» β (πΎ β (Baseβπ) β§ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin))) |
16 | 14, 15 | mpbid 231 |
. . . 4
β’ (π β (πΎ β (Baseβπ) β§ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin)) |
17 | 16 | simpld 496 |
. . 3
β’ (π β πΎ β (Baseβπ)) |
18 | 1, 2, 3, 4, 5, 6, 13, 17 | prdsplusgcl 18592 |
. 2
β’ (π β (π½ + πΎ) β (Baseβπ)) |
19 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΌ) β π β π) |
20 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΌ) β πΌ β π) |
21 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΌ) β π
Fn πΌ) |
22 | 13 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΌ) β π½ β (Baseβπ)) |
23 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΌ) β πΎ β (Baseβπ)) |
24 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β πΌ) β π β πΌ) |
25 | 1, 2, 19, 20, 21, 22, 23, 3, 24 | prdsplusgfval 17361 |
. . . . 5
β’ ((π β§ π β πΌ) β ((π½ + πΎ)βπ) = ((π½βπ)(+gβ(π
βπ))(πΎβπ))) |
26 | 25 | neeq1d 3000 |
. . . 4
β’ ((π β§ π β πΌ) β (((π½ + πΎ)βπ) β (0gβ(π
βπ)) β ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ)))) |
27 | 26 | rabbidva 3413 |
. . 3
β’ (π β {π β πΌ β£ ((π½ + πΎ)βπ) β (0gβ(π
βπ))} = {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))}) |
28 | 12 | simprd 497 |
. . . . 5
β’ (π β {π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin) |
29 | 16 | simprd 497 |
. . . . 5
β’ (π β {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin) |
30 | | unfi 9119 |
. . . . 5
β’ (({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin β§ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin) β ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))}) β Fin) |
31 | 28, 29, 30 | syl2anc 585 |
. . . 4
β’ (π β ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))}) β Fin) |
32 | | neorian 3036 |
. . . . . . . . . 10
β’ (((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ))) β Β¬ ((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ)))) |
33 | 32 | bicomi 223 |
. . . . . . . . 9
β’ (Β¬
((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ)))) |
34 | 33 | con1bii 357 |
. . . . . . . 8
β’ (Β¬
((π½βπ) β
(0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ))) β ((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ)))) |
35 | 6 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (π
βπ) β Mnd) |
36 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβ(π
βπ)) = (Baseβ(π
βπ)) |
37 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβ(π
βπ)) = (0gβ(π
βπ)) |
38 | 36, 37 | mndidcl 18576 |
. . . . . . . . . 10
β’ ((π
βπ) β Mnd β
(0gβ(π
βπ)) β (Baseβ(π
βπ))) |
39 | | eqid 2733 |
. . . . . . . . . . 11
β’
(+gβ(π
βπ)) = (+gβ(π
βπ)) |
40 | 36, 39, 37 | mndlid 18581 |
. . . . . . . . . 10
β’ (((π
βπ) β Mnd β§
(0gβ(π
βπ)) β (Baseβ(π
βπ))) β ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ))) = (0gβ(π
βπ))) |
41 | 35, 38, 40 | syl2anc2 586 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ))) = (0gβ(π
βπ))) |
42 | | oveq12 7367 |
. . . . . . . . . 10
β’ (((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β ((π½βπ)(+gβ(π
βπ))(πΎβπ)) = ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ)))) |
43 | 42 | eqeq1d 2735 |
. . . . . . . . 9
β’ (((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β (((π½βπ)(+gβ(π
βπ))(πΎβπ)) = (0gβ(π
βπ)) β ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ))) = (0gβ(π
βπ)))) |
44 | 41, 43 | syl5ibrcom 247 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β ((π½βπ)(+gβ(π
βπ))(πΎβπ)) = (0gβ(π
βπ)))) |
45 | 34, 44 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π β πΌ) β (Β¬ ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ))) β ((π½βπ)(+gβ(π
βπ))(πΎβπ)) = (0gβ(π
βπ)))) |
46 | 45 | necon1ad 2957 |
. . . . . 6
β’ ((π β§ π β πΌ) β (((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ)) β ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ))))) |
47 | 46 | ss2rabdv 4034 |
. . . . 5
β’ (π β {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))} β {π β πΌ β£ ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ)))}) |
48 | | unrab 4266 |
. . . . 5
β’ ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))}) = {π β πΌ β£ ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ)))} |
49 | 47, 48 | sseqtrrdi 3996 |
. . . 4
β’ (π β {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))} β ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))})) |
50 | 31, 49 | ssfid 9214 |
. . 3
β’ (π β {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))} β Fin) |
51 | 27, 50 | eqeltrd 2834 |
. 2
β’ (π β {π β πΌ β£ ((π½ + πΎ)βπ) β (0gβ(π
βπ))} β Fin) |
52 | 1, 8, 2, 9, 5, 10 | dsmmelbas 21161 |
. 2
β’ (π β ((π½ + πΎ) β π» β ((π½ + πΎ) β (Baseβπ) β§ {π β πΌ β£ ((π½ + πΎ)βπ) β (0gβ(π
βπ))} β Fin))) |
53 | 18, 51, 52 | mpbir2and 712 |
1
β’ (π β (π½ + πΎ) β π») |