Description: The field of real numbers is the scalar field of the generalized real Euclidean space. (Contributed by AV, 15-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rrxsca.r | |
|
Assertion | rrxsca | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rrxsca.r | |
|
2 | eqid | |
|
3 | 1 2 | rrxprds | |
4 | 3 | fveq2d | |
5 | fvex | |
|
6 | 5 | mptex | |
7 | eqid | |
|
8 | eqid | |
|
9 | 7 8 | tngsca | |
10 | 9 | eqcomd | |
11 | 6 10 | mp1i | |
12 | eqid | |
|
13 | eqid | |
|
14 | eqid | |
|
15 | 12 13 14 | tcphval | |
16 | 15 | fveq2i | |
17 | 16 | a1i | |
18 | eqid | |
|
19 | refld | |
|
20 | 19 | a1i | |
21 | id | |
|
22 | snex | |
|
23 | 22 | a1i | |
24 | 21 23 | xpexd | |
25 | 18 20 24 | prdssca | |
26 | fvex | |
|
27 | eqid | |
|
28 | eqid | |
|
29 | 27 28 | resssca | |
30 | 26 29 | mp1i | |
31 | 25 30 | eqtrd | |
32 | 11 17 31 | 3eqtr4d | |
33 | 4 32 | eqtrd | |