Step | Hyp | Ref
| Expression |
1 | | dvdivcncf.s |
. . 3
β’ (π β π β {β, β}) |
2 | | dvdivcncf.f |
. . 3
β’ (π β πΉ:πβΆβ) |
3 | | dvdivcncf.g |
. . 3
β’ (π β πΊ:πβΆ(β β
{0})) |
4 | | dvdivcncf.fdv |
. . . 4
β’ (π β (π D πΉ) β (πβcnββ)) |
5 | | cncff 24279 |
. . . 4
β’ ((π D πΉ) β (πβcnββ) β (π D πΉ):πβΆβ) |
6 | | fdm 6681 |
. . . 4
β’ ((π D πΉ):πβΆβ β dom (π D πΉ) = π) |
7 | 4, 5, 6 | 3syl 18 |
. . 3
β’ (π β dom (π D πΉ) = π) |
8 | | dvdivcncf.gdv |
. . . 4
β’ (π β (π D πΊ) β (πβcnββ)) |
9 | | cncff 24279 |
. . . 4
β’ ((π D πΊ) β (πβcnββ) β (π D πΊ):πβΆβ) |
10 | | fdm 6681 |
. . . 4
β’ ((π D πΊ):πβΆβ β dom (π D πΊ) = π) |
11 | 8, 9, 10 | 3syl 18 |
. . 3
β’ (π β dom (π D πΊ) = π) |
12 | 1, 2, 3, 7, 11 | dvdivf 44253 |
. 2
β’ (π β (π D (πΉ βf / πΊ)) = ((((π D πΉ) βf Β· πΊ) βf β
((π D πΊ) βf Β· πΉ)) βf / (πΊ βf Β·
πΊ))) |
13 | | ax-resscn 11116 |
. . . . . . . . 9
β’ β
β β |
14 | | sseq1 3973 |
. . . . . . . . 9
β’ (π = β β (π β β β β
β β)) |
15 | 13, 14 | mpbiri 258 |
. . . . . . . 8
β’ (π = β β π β
β) |
16 | | eqimss 4004 |
. . . . . . . 8
β’ (π = β β π β
β) |
17 | 15, 16 | pm3.2i 472 |
. . . . . . 7
β’ ((π = β β π β β) β§ (π = β β π β
β)) |
18 | | elpri 4612 |
. . . . . . . 8
β’ (π β {β, β}
β (π = β β¨
π =
β)) |
19 | 1, 18 | syl 17 |
. . . . . . 7
β’ (π β (π = β β¨ π = β)) |
20 | | pm3.44 959 |
. . . . . . 7
β’ (((π = β β π β β) β§ (π = β β π β β)) β
((π = β β¨ π = β) β π β
β)) |
21 | 17, 19, 20 | mpsyl 68 |
. . . . . 6
β’ (π β π β β) |
22 | | difssd 4096 |
. . . . . . 7
β’ (π β (β β {0})
β β) |
23 | 3, 22 | fssd 6690 |
. . . . . 6
β’ (π β πΊ:πβΆβ) |
24 | | dvbsss 25289 |
. . . . . . 7
β’ dom
(π D πΉ) β π |
25 | 7, 24 | eqsstrrdi 4003 |
. . . . . 6
β’ (π β π β π) |
26 | | dvcn 25308 |
. . . . . 6
β’ (((π β β β§ πΊ:πβΆβ β§ π β π) β§ dom (π D πΊ) = π) β πΊ β (πβcnββ)) |
27 | 21, 23, 25, 11, 26 | syl31anc 1374 |
. . . . 5
β’ (π β πΊ β (πβcnββ)) |
28 | 4, 27 | mulcncff 44201 |
. . . 4
β’ (π β ((π D πΉ) βf Β· πΊ) β (πβcnββ)) |
29 | | dvcn 25308 |
. . . . . 6
β’ (((π β β β§ πΉ:πβΆβ β§ π β π) β§ dom (π D πΉ) = π) β πΉ β (πβcnββ)) |
30 | 21, 2, 25, 7, 29 | syl31anc 1374 |
. . . . 5
β’ (π β πΉ β (πβcnββ)) |
31 | 8, 30 | mulcncff 44201 |
. . . 4
β’ (π β ((π D πΊ) βf Β· πΉ) β (πβcnββ)) |
32 | 28, 31 | subcncff 44211 |
. . 3
β’ (π β (((π D πΉ) βf Β· πΊ) βf β
((π D πΊ) βf Β· πΉ)) β (πβcnββ)) |
33 | | eldifi 4090 |
. . . . . . . . 9
β’ (π₯ β (β β {0})
β π₯ β
β) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β π₯
β β) |
35 | | eldifi 4090 |
. . . . . . . . 9
β’ (π¦ β (β β {0})
β π¦ β
β) |
36 | 35 | adantl 483 |
. . . . . . . 8
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β π¦
β β) |
37 | 34, 36 | mulcld 11183 |
. . . . . . 7
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β (π₯
Β· π¦) β
β) |
38 | | eldifsni 4754 |
. . . . . . . . 9
β’ (π₯ β (β β {0})
β π₯ β
0) |
39 | 38 | adantr 482 |
. . . . . . . 8
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β π₯ β
0) |
40 | | eldifsni 4754 |
. . . . . . . . 9
β’ (π¦ β (β β {0})
β π¦ β
0) |
41 | 40 | adantl 483 |
. . . . . . . 8
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β π¦ β
0) |
42 | 34, 36, 39, 41 | mulne0d 11815 |
. . . . . . 7
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β (π₯
Β· π¦) β
0) |
43 | | eldifsn 4751 |
. . . . . . 7
β’ ((π₯ Β· π¦) β (β β {0}) β ((π₯ Β· π¦) β β β§ (π₯ Β· π¦) β 0)) |
44 | 37, 42, 43 | sylanbrc 584 |
. . . . . 6
β’ ((π₯ β (β β {0})
β§ π¦ β (β
β {0})) β (π₯
Β· π¦) β (β
β {0})) |
45 | 44 | adantl 483 |
. . . . 5
β’ ((π β§ (π₯ β (β β {0}) β§ π¦ β (β β {0})))
β (π₯ Β· π¦) β (β β
{0})) |
46 | 1, 25 | ssexd 5285 |
. . . . 5
β’ (π β π β V) |
47 | | inidm 4182 |
. . . . 5
β’ (π β© π) = π |
48 | 45, 3, 3, 46, 46, 47 | off 7639 |
. . . 4
β’ (π β (πΊ βf Β· πΊ):πβΆ(β β
{0})) |
49 | 27, 27 | mulcncff 44201 |
. . . . 5
β’ (π β (πΊ βf Β· πΊ) β (πβcnββ)) |
50 | | cncfcdm 24284 |
. . . . 5
β’
(((β β {0}) β β β§ (πΊ βf Β· πΊ) β (πβcnββ)) β ((πΊ βf Β· πΊ) β (πβcnβ(β β {0})) β (πΊ βf Β· πΊ):πβΆ(β β
{0}))) |
51 | 22, 49, 50 | syl2anc 585 |
. . . 4
β’ (π β ((πΊ βf Β· πΊ) β (πβcnβ(β β {0})) β (πΊ βf Β· πΊ):πβΆ(β β
{0}))) |
52 | 48, 51 | mpbird 257 |
. . 3
β’ (π β (πΊ βf Β· πΊ) β (πβcnβ(β β {0}))) |
53 | 32, 52 | divcncff 44222 |
. 2
β’ (π β ((((π D πΉ) βf Β· πΊ) βf β
((π D πΊ) βf Β· πΉ)) βf / (πΊ βf Β·
πΊ)) β (πβcnββ)) |
54 | 12, 53 | eqeltrd 2834 |
1
β’ (π β (π D (πΉ βf / πΊ)) β (πβcnββ)) |