Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’ ran πΊ = ran πΊ |
2 | 1 | isgrpo 29488 |
. . . 4
β’ (πΊ β GrpOp β (πΊ β GrpOp β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ€ β ran πΊβπ₯ β ran πΊ((π€πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π€)))) |
3 | 2 | biimpd 228 |
. . 3
β’ (πΊ β GrpOp β (πΊ β GrpOp β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ€ β ran πΊβπ₯ β ran πΊ((π€πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π€)))) |
4 | 1 | grpoidinv 29499 |
. . . . . . . 8
β’ (πΊ β GrpOp β
βπ₯ β ran πΊβπ¦ β ran πΊ(((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β§ βπ€ β ran πΊ((π€πΊπ¦) = π₯ β§ (π¦πΊπ€) = π₯))) |
5 | | simpl 484 |
. . . . . . . . . . 11
β’ ((((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β§ βπ€ β ran πΊ((π€πΊπ¦) = π₯ β§ (π¦πΊπ€) = π₯)) β ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)) |
6 | 5 | ralimi 3083 |
. . . . . . . . . 10
β’
(βπ¦ β
ran πΊ(((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β§ βπ€ β ran πΊ((π€πΊπ¦) = π₯ β§ (π¦πΊπ€) = π₯)) β βπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)) |
7 | 6 | reximi 3084 |
. . . . . . . . 9
β’
(βπ₯ β ran
πΊβπ¦ β ran πΊ(((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β§ βπ€ β ran πΊ((π€πΊπ¦) = π₯ β§ (π¦πΊπ€) = π₯)) β βπ₯ β ran πΊβπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)) |
8 | 1 | ismndo2 36383 |
. . . . . . . . . . . . 13
β’ (πΊ β GrpOp β (πΊ β MndOp β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) |
9 | 8 | biimprcd 250 |
. . . . . . . . . . . 12
β’ ((πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)) β (πΊ β GrpOp β πΊ β MndOp)) |
10 | 9 | 3exp 1120 |
. . . . . . . . . . 11
β’ (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β (βπ₯ β ran πΊβπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β (πΊ β GrpOp β πΊ β MndOp)))) |
11 | 10 | impcom 409 |
. . . . . . . . . 10
β’
((βπ₯ β
ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ) β (βπ₯ β ran πΊβπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β (πΊ β GrpOp β πΊ β MndOp))) |
12 | 11 | com3l 89 |
. . . . . . . . 9
β’
(βπ₯ β ran
πΊβπ¦ β ran πΊ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β (πΊ β GrpOp β ((βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ) β πΊ β MndOp))) |
13 | 7, 12 | syl 17 |
. . . . . . . 8
β’
(βπ₯ β ran
πΊβπ¦ β ran πΊ(((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦) β§ βπ€ β ran πΊ((π€πΊπ¦) = π₯ β§ (π¦πΊπ€) = π₯)) β (πΊ β GrpOp β ((βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ) β πΊ β MndOp))) |
14 | 4, 13 | mpcom 38 |
. . . . . . 7
β’ (πΊ β GrpOp β
((βπ₯ β ran
πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ) β πΊ β MndOp)) |
15 | 14 | expdcom 416 |
. . . . . 6
β’
(βπ₯ β
ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β (πΊ β GrpOp β πΊ β MndOp))) |
16 | 15 | a1i 11 |
. . . . 5
β’
(βπ€ β ran
πΊβπ₯ β ran πΊ((π€πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π€) β (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β (πΊ β GrpOp β πΊ β MndOp)))) |
17 | 16 | com13 88 |
. . . 4
β’ (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β (βπ€ β ran πΊβπ₯ β ran πΊ((π€πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π€) β (πΊ β GrpOp β πΊ β MndOp)))) |
18 | 17 | 3imp 1112 |
. . 3
β’ ((πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ€ β ran πΊβπ₯ β ran πΊ((π€πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π€)) β (πΊ β GrpOp β πΊ β MndOp)) |
19 | 3, 18 | syli 39 |
. 2
β’ (πΊ β GrpOp β (πΊ β GrpOp β πΊ β MndOp)) |
20 | 19 | pm2.43i 52 |
1
β’ (πΊ β GrpOp β πΊ β MndOp) |