Step | Hyp | Ref
| Expression |
1 | | isgrpda.2 |
. . 3
β’ (π β πΊ:(π Γ π)βΆπ) |
2 | | isgrpda.3 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) |
3 | 2 | ralrimivvva 3200 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) |
4 | | isgrpda.4 |
. . . 4
β’ (π β π β π) |
5 | | isgrpda.5 |
. . . . . 6
β’ ((π β§ π₯ β π) β (ππΊπ₯) = π₯) |
6 | | isgrpda.6 |
. . . . . . 7
β’ ((π β§ π₯ β π) β βπ β π (ππΊπ₯) = π) |
7 | | oveq1 7364 |
. . . . . . . . 9
β’ (π¦ = π β (π¦πΊπ₯) = (ππΊπ₯)) |
8 | 7 | eqeq1d 2738 |
. . . . . . . 8
β’ (π¦ = π β ((π¦πΊπ₯) = π β (ππΊπ₯) = π)) |
9 | 8 | cbvrexvw 3226 |
. . . . . . 7
β’
(βπ¦ β
π (π¦πΊπ₯) = π β βπ β π (ππΊπ₯) = π) |
10 | 6, 9 | sylibr 233 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π (π¦πΊπ₯) = π) |
11 | 5, 10 | jca 512 |
. . . . 5
β’ ((π β§ π₯ β π) β ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π)) |
12 | 11 | ralrimiva 3143 |
. . . 4
β’ (π β βπ₯ β π ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π)) |
13 | | oveq1 7364 |
. . . . . . . 8
β’ (π’ = π β (π’πΊπ₯) = (ππΊπ₯)) |
14 | 13 | eqeq1d 2738 |
. . . . . . 7
β’ (π’ = π β ((π’πΊπ₯) = π₯ β (ππΊπ₯) = π₯)) |
15 | | eqeq2 2748 |
. . . . . . . 8
β’ (π’ = π β ((π¦πΊπ₯) = π’ β (π¦πΊπ₯) = π)) |
16 | 15 | rexbidv 3175 |
. . . . . . 7
β’ (π’ = π β (βπ¦ β π (π¦πΊπ₯) = π’ β βπ¦ β π (π¦πΊπ₯) = π)) |
17 | 14, 16 | anbi12d 631 |
. . . . . 6
β’ (π’ = π β (((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’) β ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π))) |
18 | 17 | ralbidv 3174 |
. . . . 5
β’ (π’ = π β (βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’) β βπ₯ β π ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π))) |
19 | 18 | rspcev 3581 |
. . . 4
β’ ((π β π β§ βπ₯ β π ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π)) β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’)) |
20 | 4, 12, 19 | syl2anc 584 |
. . 3
β’ (π β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’)) |
21 | 4 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π β π) |
22 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π₯ β π) |
23 | 5 | eqcomd 2742 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π₯ = (ππΊπ₯)) |
24 | | rspceov 7404 |
. . . . . . . . . 10
β’ ((π β π β§ π₯ β π β§ π₯ = (ππΊπ₯)) β βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§)) |
25 | 21, 22, 23, 24 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§)) |
26 | 25 | ralrimiva 3143 |
. . . . . . . 8
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§)) |
27 | | foov 7528 |
. . . . . . . 8
β’ (πΊ:(π Γ π)βontoβπ β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§))) |
28 | 1, 26, 27 | sylanbrc 583 |
. . . . . . 7
β’ (π β πΊ:(π Γ π)βontoβπ) |
29 | | forn 6759 |
. . . . . . 7
β’ (πΊ:(π Γ π)βontoβπ β ran πΊ = π) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’ (π β ran πΊ = π) |
31 | 30 | sqxpeqd 5665 |
. . . . 5
β’ (π β (ran πΊ Γ ran πΊ) = (π Γ π)) |
32 | 31, 30 | feq23d 6663 |
. . . 4
β’ (π β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β πΊ:(π Γ π)βΆπ)) |
33 | 30 | raleqdv 3313 |
. . . . . 6
β’ (π β (βπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) |
34 | 30, 33 | raleqbidv 3319 |
. . . . 5
β’ (π β (βπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) |
35 | 30, 34 | raleqbidv 3319 |
. . . 4
β’ (π β (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) |
36 | 30 | rexeqdv 3314 |
. . . . . . 7
β’ (π β (βπ¦ β ran πΊ(π¦πΊπ₯) = π’ β βπ¦ β π (π¦πΊπ₯) = π’)) |
37 | 36 | anbi2d 629 |
. . . . . 6
β’ (π β (((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’) β ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’))) |
38 | 30, 37 | raleqbidv 3319 |
. . . . 5
β’ (π β (βπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’) β βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’))) |
39 | 30, 38 | rexeqbidv 3320 |
. . . 4
β’ (π β (βπ’ β ran πΊβπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’) β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’))) |
40 | 32, 35, 39 | 3anbi123d 1436 |
. . 3
β’ (π β ((πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ’ β ran πΊβπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’)) β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’)))) |
41 | 1, 3, 20, 40 | mpbir3and 1342 |
. 2
β’ (π β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ’ β ran πΊβπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’))) |
42 | | isgrpda.1 |
. . . . 5
β’ (π β π β V) |
43 | 42, 42 | xpexd 7685 |
. . . 4
β’ (π β (π Γ π) β V) |
44 | 1, 43 | fexd 7177 |
. . 3
β’ (π β πΊ β V) |
45 | | eqid 2736 |
. . . 4
β’ ran πΊ = ran πΊ |
46 | 45 | isgrpo 29439 |
. . 3
β’ (πΊ β V β (πΊ β GrpOp β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ’ β ran πΊβπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’)))) |
47 | 44, 46 | syl 17 |
. 2
β’ (π β (πΊ β GrpOp β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β§ βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ’ β ran πΊβπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’)))) |
48 | 41, 47 | mpbird 256 |
1
β’ (π β πΊ β GrpOp) |