Step | Hyp | Ref
| Expression |
1 | | dsmmcl.p |
. . 3
β’ π = (πXsπ
) |
2 | | eqid 2732 |
. . 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 2732 |
. . . . . 6
β’ (π βm π
) = (π βm π
) |
9 | | dsmmcl.h |
. . . . . 6
β’ π» = (Baseβ(π βm π
)) |
10 | 6 | ffnd 6718 |
. . . . . 6
β’ (π β π
Fn πΌ) |
11 | 1, 8, 2, 9, 5, 10 | dsmmelbas 21293 |
. . . . 5
β’ (π β (π½ β π» β (π½ β (Baseβπ) β§ {π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin))) |
12 | 7, 11 | mpbid 231 |
. . . 4
β’ (π β (π½ β (Baseβπ) β§ {π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin)) |
13 | 12 | simpld 495 |
. . 3
β’ (π β π½ β (Baseβπ)) |
14 | | dsmmacl.k |
. . . . 5
β’ (π β πΎ β π») |
15 | 1, 8, 2, 9, 5, 10 | dsmmelbas 21293 |
. . . . 5
β’ (π β (πΎ β π» β (πΎ β (Baseβπ) β§ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin))) |
16 | 14, 15 | mpbid 231 |
. . . 4
β’ (π β (πΎ β (Baseβπ) β§ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin)) |
17 | 16 | simpld 495 |
. . 3
β’ (π β πΎ β (Baseβπ)) |
18 | 1, 2, 3, 4, 5, 6, 13, 17 | prdsplusgcl 18655 |
. 2
β’ (π β (π½ + πΎ) β (Baseβπ)) |
19 | 4 | adantr 481 |
. . . . . 6
β’ ((π β§ π β πΌ) β π β π) |
20 | 5 | adantr 481 |
. . . . . 6
β’ ((π β§ π β πΌ) β πΌ β π) |
21 | 10 | adantr 481 |
. . . . . 6
β’ ((π β§ π β πΌ) β π
Fn πΌ) |
22 | 13 | adantr 481 |
. . . . . 6
β’ ((π β§ π β πΌ) β π½ β (Baseβπ)) |
23 | 17 | adantr 481 |
. . . . . 6
β’ ((π β§ π β πΌ) β πΎ β (Baseβπ)) |
24 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β πΌ) β π β πΌ) |
25 | 1, 2, 19, 20, 21, 22, 23, 3, 24 | prdsplusgfval 17419 |
. . . . 5
β’ ((π β§ π β πΌ) β ((π½ + πΎ)βπ) = ((π½βπ)(+gβ(π
βπ))(πΎβπ))) |
26 | 25 | neeq1d 3000 |
. . . 4
β’ ((π β§ π β πΌ) β (((π½ + πΎ)βπ) β (0gβ(π
βπ)) β ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ)))) |
27 | 26 | rabbidva 3439 |
. . 3
β’ (π β {π β πΌ β£ ((π½ + πΎ)βπ) β (0gβ(π
βπ))} = {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))}) |
28 | 12 | simprd 496 |
. . . . 5
β’ (π β {π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin) |
29 | 16 | simprd 496 |
. . . . 5
β’ (π β {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin) |
30 | | unfi 9171 |
. . . . 5
β’ (({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} β Fin β§ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))} β Fin) β ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))}) β Fin) |
31 | 28, 29, 30 | syl2anc 584 |
. . . 4
β’ (π β ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))}) β Fin) |
32 | | neorian 3037 |
. . . . . . . . . 10
β’ (((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ))) β Β¬ ((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ)))) |
33 | 32 | bicomi 223 |
. . . . . . . . 9
β’ (Β¬
((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ)))) |
34 | 33 | con1bii 356 |
. . . . . . . 8
β’ (Β¬
((π½βπ) β
(0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ))) β ((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ)))) |
35 | 6 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (π
βπ) β Mnd) |
36 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβ(π
βπ)) = (Baseβ(π
βπ)) |
37 | | eqid 2732 |
. . . . . . . . . . 11
β’
(0gβ(π
βπ)) = (0gβ(π
βπ)) |
38 | 36, 37 | mndidcl 18639 |
. . . . . . . . . 10
β’ ((π
βπ) β Mnd β
(0gβ(π
βπ)) β (Baseβ(π
βπ))) |
39 | | eqid 2732 |
. . . . . . . . . . 11
β’
(+gβ(π
βπ)) = (+gβ(π
βπ)) |
40 | 36, 39, 37 | mndlid 18644 |
. . . . . . . . . 10
β’ (((π
βπ) β Mnd β§
(0gβ(π
βπ)) β (Baseβ(π
βπ))) β ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ))) = (0gβ(π
βπ))) |
41 | 35, 38, 40 | syl2anc2 585 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ))) = (0gβ(π
βπ))) |
42 | | oveq12 7417 |
. . . . . . . . . 10
β’ (((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β ((π½βπ)(+gβ(π
βπ))(πΎβπ)) = ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ)))) |
43 | 42 | eqeq1d 2734 |
. . . . . . . . 9
β’ (((π½βπ) = (0gβ(π
βπ)) β§ (πΎβπ) = (0gβ(π
βπ))) β (((π½βπ)(+gβ(π
βπ))(πΎβπ)) = (0gβ(π
βπ)) β ((0gβ(π
βπ))(+gβ(π
βπ))(0gβ(π
βπ))) = (0gβ(π
βπ)))) |
44 | 41, 43 | syl5ibrcom 246 |
. . . . . . . 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 4073 |
. . . . 5
β’ (π β {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))} β {π β πΌ β£ ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ)))}) |
48 | | unrab 4305 |
. . . . 5
β’ ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))}) = {π β πΌ β£ ((π½βπ) β (0gβ(π
βπ)) β¨ (πΎβπ) β (0gβ(π
βπ)))} |
49 | 47, 48 | sseqtrrdi 4033 |
. . . 4
β’ (π β {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))} β ({π β πΌ β£ (π½βπ) β (0gβ(π
βπ))} βͺ {π β πΌ β£ (πΎβπ) β (0gβ(π
βπ))})) |
50 | 31, 49 | ssfid 9266 |
. . 3
β’ (π β {π β πΌ β£ ((π½βπ)(+gβ(π
βπ))(πΎβπ)) β (0gβ(π
βπ))} β Fin) |
51 | 27, 50 | eqeltrd 2833 |
. 2
β’ (π β {π β πΌ β£ ((π½ + πΎ)βπ) β (0gβ(π
βπ))} β Fin) |
52 | 1, 8, 2, 9, 5, 10 | dsmmelbas 21293 |
. 2
β’ (π β ((π½ + πΎ) β π» β ((π½ + πΎ) β (Baseβπ) β§ {π β πΌ β£ ((π½ + πΎ)βπ) β (0gβ(π
βπ))} β Fin))) |
53 | 18, 51, 52 | mpbir2and 711 |
1
β’ (π β (π½ + πΎ) β π») |