Step | Hyp | Ref
| Expression |
1 | | isgrpda.2 |
. . 3
β’ (π β πΊ:(π Γ π)βΆπ) |
2 | | isgrpda.3 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) |
3 | 2 | ralrimivvva 3203 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) |
4 | | isgrpda.4 |
. . . 4
β’ (π β π β π) |
5 | | isgrpda.5 |
. . . . . 6
β’ ((π β§ π₯ β π) β (ππΊπ₯) = π₯) |
6 | | isgrpda.6 |
. . . . . . 7
β’ ((π β§ π₯ β π) β βπ β π (ππΊπ₯) = π) |
7 | | oveq1 7415 |
. . . . . . . . 9
β’ (π¦ = π β (π¦πΊπ₯) = (ππΊπ₯)) |
8 | 7 | eqeq1d 2734 |
. . . . . . . 8
β’ (π¦ = π β ((π¦πΊπ₯) = π β (ππΊπ₯) = π)) |
9 | 8 | cbvrexvw 3235 |
. . . . . . 7
β’
(βπ¦ β
π (π¦πΊπ₯) = π β βπ β π (ππΊπ₯) = π) |
10 | 6, 9 | sylibr 233 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π (π¦πΊπ₯) = π) |
11 | 5, 10 | jca 512 |
. . . . 5
β’ ((π β§ π₯ β π) β ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π)) |
12 | 11 | ralrimiva 3146 |
. . . 4
β’ (π β βπ₯ β π ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π)) |
13 | | oveq1 7415 |
. . . . . . . 8
β’ (π’ = π β (π’πΊπ₯) = (ππΊπ₯)) |
14 | 13 | eqeq1d 2734 |
. . . . . . 7
β’ (π’ = π β ((π’πΊπ₯) = π₯ β (ππΊπ₯) = π₯)) |
15 | | eqeq2 2744 |
. . . . . . . 8
β’ (π’ = π β ((π¦πΊπ₯) = π’ β (π¦πΊπ₯) = π)) |
16 | 15 | rexbidv 3178 |
. . . . . . 7
β’ (π’ = π β (βπ¦ β π (π¦πΊπ₯) = π’ β βπ¦ β π (π¦πΊπ₯) = π)) |
17 | 14, 16 | anbi12d 631 |
. . . . . 6
β’ (π’ = π β (((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’) β ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π))) |
18 | 17 | ralbidv 3177 |
. . . . 5
β’ (π’ = π β (βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’) β βπ₯ β π ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π))) |
19 | 18 | rspcev 3612 |
. . . 4
β’ ((π β π β§ βπ₯ β π ((ππΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π)) β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’)) |
20 | 4, 12, 19 | syl2anc 584 |
. . 3
β’ (π β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’)) |
21 | 4 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π β π) |
22 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π₯ β π) |
23 | 5 | eqcomd 2738 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π₯ = (ππΊπ₯)) |
24 | | rspceov 7455 |
. . . . . . . . . 10
β’ ((π β π β§ π₯ β π β§ π₯ = (ππΊπ₯)) β βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§)) |
25 | 21, 22, 23, 24 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§)) |
26 | 25 | ralrimiva 3146 |
. . . . . . . 8
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§)) |
27 | | foov 7580 |
. . . . . . . 8
β’ (πΊ:(π Γ π)βontoβπ β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π π₯ = (π¦πΊπ§))) |
28 | 1, 26, 27 | sylanbrc 583 |
. . . . . . 7
β’ (π β πΊ:(π Γ π)βontoβπ) |
29 | | forn 6808 |
. . . . . . 7
β’ (πΊ:(π Γ π)βontoβπ β ran πΊ = π) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’ (π β ran πΊ = π) |
31 | 30 | sqxpeqd 5708 |
. . . . 5
β’ (π β (ran πΊ Γ ran πΊ) = (π Γ π)) |
32 | 31, 30 | feq23d 6712 |
. . . 4
β’ (π β (πΊ:(ran πΊ Γ ran πΊ)βΆran πΊ β πΊ:(π Γ π)βΆπ)) |
33 | 30 | raleqdv 3325 |
. . . . . 6
β’ (π β (βπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) |
34 | 30, 33 | raleqbidv 3342 |
. . . . 5
β’ (π β (βπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) |
35 | 30, 34 | raleqbidv 3342 |
. . . 4
β’ (π β (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) |
36 | 30 | rexeqdv 3326 |
. . . . . . 7
β’ (π β (βπ¦ β ran πΊ(π¦πΊπ₯) = π’ β βπ¦ β π (π¦πΊπ₯) = π’)) |
37 | 36 | anbi2d 629 |
. . . . . 6
β’ (π β (((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’) β ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’))) |
38 | 30, 37 | raleqbidv 3342 |
. . . . 5
β’ (π β (βπ₯ β ran πΊ((π’πΊπ₯) = π₯ β§ βπ¦ β ran πΊ(π¦πΊπ₯) = π’) β βπ₯ β π ((π’πΊπ₯) = π₯ β§ βπ¦ β π (π¦πΊπ₯) = π’))) |
39 | 30, 38 | rexeqbidv 3343 |
. . . 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 7737 |
. . . 4
β’ (π β (π Γ π) β V) |
44 | 1, 43 | fexd 7228 |
. . 3
β’ (π β πΊ β V) |
45 | | eqid 2732 |
. . . 4
β’ ran πΊ = ran πΊ |
46 | 45 | isgrpo 29745 |
. . 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) |