Step | Hyp | Ref
| Expression |
1 | | df-obs 20049 |
. . . . 5
OBasis Scalar Scalar |
2 | 1 | dmmptss 5631 |
. . . 4
OBasis |
3 | | elfvdm 6220 |
. . . 4
OBasis
OBasis |
4 | 2, 3 | sseldi 3601 |
. . 3
OBasis
|
5 | | fveq2 6191 |
. . . . . . . . 9
|
6 | | isobs.v |
. . . . . . . . 9
|
7 | 5, 6 | syl6eqr 2674 |
. . . . . . . 8
|
8 | 7 | pweqd 4163 |
. . . . . . 7
|
9 | | fveq2 6191 |
. . . . . . . . . . . 12
|
10 | | isobs.h |
. . . . . . . . . . . 12
|
11 | 9, 10 | syl6eqr 2674 |
. . . . . . . . . . 11
|
12 | 11 | oveqd 6667 |
. . . . . . . . . 10
|
13 | | fveq2 6191 |
. . . . . . . . . . . . . 14
Scalar Scalar |
14 | | isobs.f |
. . . . . . . . . . . . . 14
Scalar |
15 | 13, 14 | syl6eqr 2674 |
. . . . . . . . . . . . 13
Scalar |
16 | 15 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar |
17 | | isobs.u |
. . . . . . . . . . . 12
|
18 | 16, 17 | syl6eqr 2674 |
. . . . . . . . . . 11
Scalar |
19 | 15 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar |
20 | | isobs.z |
. . . . . . . . . . . 12
|
21 | 19, 20 | syl6eqr 2674 |
. . . . . . . . . . 11
Scalar |
22 | 18, 21 | ifeq12d 4106 |
. . . . . . . . . 10
Scalar Scalar |
23 | 12, 22 | eqeq12d 2637 |
. . . . . . . . 9
Scalar Scalar |
24 | 23 | 2ralbidv 2989 |
. . . . . . . 8
Scalar Scalar
|
25 | | fveq2 6191 |
. . . . . . . . . . 11
|
26 | | isobs.o |
. . . . . . . . . . 11
|
27 | 25, 26 | syl6eqr 2674 |
. . . . . . . . . 10
|
28 | 27 | fveq1d 6193 |
. . . . . . . . 9
|
29 | | fveq2 6191 |
. . . . . . . . . . 11
|
30 | | isobs.y |
. . . . . . . . . . 11
|
31 | 29, 30 | syl6eqr 2674 |
. . . . . . . . . 10
|
32 | 31 | sneqd 4189 |
. . . . . . . . 9
|
33 | 28, 32 | eqeq12d 2637 |
. . . . . . . 8
|
34 | 24, 33 | anbi12d 747 |
. . . . . . 7
Scalar Scalar |
35 | 8, 34 | rabeqbidv 3195 |
. . . . . 6
Scalar Scalar
|
36 | | fvex 6201 |
. . . . . . . . 9
|
37 | 6, 36 | eqeltri 2697 |
. . . . . . . 8
|
38 | 37 | pwex 4848 |
. . . . . . 7
|
39 | 38 | rabex 4813 |
. . . . . 6
|
40 | 35, 1, 39 | fvmpt 6282 |
. . . . 5
OBasis
|
41 | 40 | eleq2d 2687 |
. . . 4
OBasis
|
42 | | raleq 3138 |
. . . . . . . 8
|
43 | 42 | raleqbi1dv 3146 |
. . . . . . 7
|
44 | | fveq2 6191 |
. . . . . . . 8
|
45 | 44 | eqeq1d 2624 |
. . . . . . 7
|
46 | 43, 45 | anbi12d 747 |
. . . . . 6
|
47 | 46 | elrab 3363 |
. . . . 5
|
48 | 37 | elpw2 4828 |
. . . . . 6
|
49 | 48 | anbi1i 731 |
. . . . 5
|
50 | 47, 49 | bitri 264 |
. . . 4
|
51 | 41, 50 | syl6bb 276 |
. . 3
OBasis
|
52 | 4, 51 | biadan2 674 |
. 2
OBasis
|
53 | | 3anass 1042 |
. 2
|
54 | 52, 53 | bitr4i 267 |
1
OBasis |