Step |
Hyp |
Ref |
Expression |
1 |
|
opprabs.o |
|- O = ( oppR ` R ) |
2 |
|
opprabs.m |
|- .x. = ( .r ` R ) |
3 |
|
opprabs.1 |
|- ( ph -> R e. V ) |
4 |
|
opprabs.2 |
|- ( ph -> Fun R ) |
5 |
|
opprabs.3 |
|- ( ph -> ( .r ` ndx ) e. dom R ) |
6 |
|
opprabs.4 |
|- ( ph -> .x. Fn ( B X. B ) ) |
7 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
8 |
|
eqid |
|- ( .r ` O ) = ( .r ` O ) |
9 |
7 2 1 8
|
opprmulfval |
|- ( .r ` O ) = tpos .x. |
10 |
9
|
tposeqi |
|- tpos ( .r ` O ) = tpos tpos .x. |
11 |
|
fnrel |
|- ( .x. Fn ( B X. B ) -> Rel .x. ) |
12 |
|
relxp |
|- Rel ( B X. B ) |
13 |
|
fndm |
|- ( .x. Fn ( B X. B ) -> dom .x. = ( B X. B ) ) |
14 |
13
|
releqd |
|- ( .x. Fn ( B X. B ) -> ( Rel dom .x. <-> Rel ( B X. B ) ) ) |
15 |
12 14
|
mpbiri |
|- ( .x. Fn ( B X. B ) -> Rel dom .x. ) |
16 |
|
tpostpos2 |
|- ( ( Rel .x. /\ Rel dom .x. ) -> tpos tpos .x. = .x. ) |
17 |
11 15 16
|
syl2anc |
|- ( .x. Fn ( B X. B ) -> tpos tpos .x. = .x. ) |
18 |
10 17
|
eqtrid |
|- ( .x. Fn ( B X. B ) -> tpos ( .r ` O ) = .x. ) |
19 |
6 18
|
syl |
|- ( ph -> tpos ( .r ` O ) = .x. ) |
20 |
19 2
|
eqtrdi |
|- ( ph -> tpos ( .r ` O ) = ( .r ` R ) ) |
21 |
20
|
opeq2d |
|- ( ph -> <. ( .r ` ndx ) , tpos ( .r ` O ) >. = <. ( .r ` ndx ) , ( .r ` R ) >. ) |
22 |
21
|
oveq2d |
|- ( ph -> ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , ( .r ` R ) >. ) ) |
23 |
1 7
|
opprbas |
|- ( Base ` R ) = ( Base ` O ) |
24 |
|
eqid |
|- ( oppR ` O ) = ( oppR ` O ) |
25 |
23 8 24
|
opprval |
|- ( oppR ` O ) = ( O sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) |
26 |
7 2 1
|
opprval |
|- O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) |
27 |
26
|
oveq1i |
|- ( O sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) |
28 |
25 27
|
eqtri |
|- ( oppR ` O ) = ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) |
29 |
|
fvex |
|- ( .r ` O ) e. _V |
30 |
29
|
tposex |
|- tpos ( .r ` O ) e. _V |
31 |
|
setsabs |
|- ( ( R e. V /\ tpos ( .r ` O ) e. _V ) -> ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) ) |
32 |
30 31
|
mpan2 |
|- ( R e. V -> ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) ) |
33 |
28 32
|
eqtrid |
|- ( R e. V -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) ) |
34 |
3 33
|
syl |
|- ( ph -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) ) |
35 |
|
mulridx |
|- .r = Slot ( .r ` ndx ) |
36 |
35 3 4 5
|
setsidvald |
|- ( ph -> R = ( R sSet <. ( .r ` ndx ) , ( .r ` R ) >. ) ) |
37 |
22 34 36
|
3eqtr4rd |
|- ( ph -> R = ( oppR ` O ) ) |