Step | Hyp | Ref
| Expression |
1 | | iscgrgd.a |
. . . . 5
β’ (π β π΄:π·βΆπ) |
2 | | iscgrgd.d |
. . . . 5
β’ (π β π· β β) |
3 | | iscgrg.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
4 | 3 | fvexi 6860 |
. . . . . 6
β’ π β V |
5 | | reex 11150 |
. . . . . 6
β’ β
β V |
6 | | elpm2r 8789 |
. . . . . 6
β’ (((π β V β§ β β
V) β§ (π΄:π·βΆπ β§ π· β β)) β π΄ β (π βpm
β)) |
7 | 4, 5, 6 | mpanl12 701 |
. . . . 5
β’ ((π΄:π·βΆπ β§ π· β β) β π΄ β (π βpm
β)) |
8 | 1, 2, 7 | syl2anc 585 |
. . . 4
β’ (π β π΄ β (π βpm
β)) |
9 | | iscgrgd.b |
. . . . 5
β’ (π β π΅:π·βΆπ) |
10 | | elpm2r 8789 |
. . . . . 6
β’ (((π β V β§ β β
V) β§ (π΅:π·βΆπ β§ π· β β)) β π΅ β (π βpm
β)) |
11 | 4, 5, 10 | mpanl12 701 |
. . . . 5
β’ ((π΅:π·βΆπ β§ π· β β) β π΅ β (π βpm
β)) |
12 | 9, 2, 11 | syl2anc 585 |
. . . 4
β’ (π β π΅ β (π βpm
β)) |
13 | 8, 12 | jca 513 |
. . 3
β’ (π β (π΄ β (π βpm β) β§ π΅ β (π βpm
β))) |
14 | 13 | biantrurd 534 |
. 2
β’ (π β ((dom π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β ((π΄ β (π βpm β) β§ π΅ β (π βpm β)) β§ (dom
π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))))) |
15 | 1 | fdmd 6683 |
. . . 4
β’ (π β dom π΄ = π·) |
16 | 9 | fdmd 6683 |
. . . 4
β’ (π β dom π΅ = π·) |
17 | 15, 16 | eqtr4d 2776 |
. . 3
β’ (π β dom π΄ = dom π΅) |
18 | 17 | biantrurd 534 |
. 2
β’ (π β (βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β (dom π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
19 | | iscgrgd.g |
. . 3
β’ (π β πΊ β π) |
20 | | iscgrg.m |
. . . 4
β’ β =
(distβπΊ) |
21 | | iscgrg.e |
. . . 4
β’ βΌ =
(cgrGβπΊ) |
22 | 3, 20, 21 | iscgrg 27503 |
. . 3
β’ (πΊ β π β (π΄ βΌ π΅ β ((π΄ β (π βpm β) β§ π΅ β (π βpm β)) β§ (dom
π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))))) |
23 | 19, 22 | syl 17 |
. 2
β’ (π β (π΄ βΌ π΅ β ((π΄ β (π βpm β) β§ π΅ β (π βpm β)) β§ (dom
π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))))) |
24 | 14, 18, 23 | 3bitr4rd 312 |
1
β’ (π β (π΄ βΌ π΅ β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |