Step |
Hyp |
Ref |
Expression |
1 |
|
ablpropd.1 |
|- ( ph -> B = ( Base ` K ) ) |
2 |
|
ablpropd.2 |
|- ( ph -> B = ( Base ` L ) ) |
3 |
|
ablpropd.3 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) |
4 |
1 2 3
|
mndpropd |
|- ( ph -> ( K e. Mnd <-> L e. Mnd ) ) |
5 |
3
|
oveqrspc2v |
|- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) ) |
6 |
3
|
oveqrspc2v |
|- ( ( ph /\ ( v e. B /\ u e. B ) ) -> ( v ( +g ` K ) u ) = ( v ( +g ` L ) u ) ) |
7 |
6
|
ancom2s |
|- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( v ( +g ` K ) u ) = ( v ( +g ` L ) u ) ) |
8 |
5 7
|
eqeq12d |
|- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) |
9 |
8
|
2ralbidva |
|- ( ph -> ( A. u e. B A. v e. B ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. u e. B A. v e. B ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) |
10 |
1
|
raleqdv |
|- ( ph -> ( A. v e. B ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) ) |
11 |
1 10
|
raleqbidv |
|- ( ph -> ( A. u e. B A. v e. B ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) ) |
12 |
2
|
raleqdv |
|- ( ph -> ( A. v e. B ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) <-> A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) |
13 |
2 12
|
raleqbidv |
|- ( ph -> ( A. u e. B A. v e. B ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) |
14 |
9 11 13
|
3bitr3d |
|- ( ph -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) |
15 |
4 14
|
anbi12d |
|- ( ph -> ( ( K e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) <-> ( L e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) ) |
16 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
17 |
|
eqid |
|- ( +g ` K ) = ( +g ` K ) |
18 |
16 17
|
iscmn |
|- ( K e. CMnd <-> ( K e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) ) |
19 |
|
eqid |
|- ( Base ` L ) = ( Base ` L ) |
20 |
|
eqid |
|- ( +g ` L ) = ( +g ` L ) |
21 |
19 20
|
iscmn |
|- ( L e. CMnd <-> ( L e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) |
22 |
15 18 21
|
3bitr4g |
|- ( ph -> ( K e. CMnd <-> L e. CMnd ) ) |