Proof of Theorem rrxip
Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . . 4
ℝ^   |
2 | | rrxbase.b |
. . . 4
     |
3 | 1, 2 | rrxprds 23177 |
. . 3
 toCHil  RRfld s   subringAlg RRfld      ↾s     |
4 | 3 | fveq2d 6195 |
. 2
        toCHil  RRfld s   subringAlg
RRfld      ↾s      |
5 | | eqid 2622 |
. . . 4
toCHil  RRfld s   subringAlg
RRfld      ↾s   toCHil  RRfld s   subringAlg
RRfld      ↾s    |
6 | | eqid 2622 |
. . . 4
    RRfld s   subringAlg RRfld      ↾s       RRfld s   subringAlg RRfld      ↾s    |
7 | 5, 6 | tchip 23024 |
. . 3
    RRfld s   subringAlg RRfld      ↾s      toCHil  RRfld s   subringAlg RRfld      ↾s     |
8 | | fvex 6201 |
. . . . . 6
     |
9 | 2, 8 | eqeltri 2697 |
. . . . 5
 |
10 | | eqid 2622 |
. . . . . 6
 RRfld s
  subringAlg RRfld      ↾s   RRfld s   subringAlg RRfld      ↾s   |
11 | | eqid 2622 |
. . . . . 6
   RRfld s   subringAlg
RRfld          RRfld s   subringAlg
RRfld        |
12 | 10, 11 | ressip 16033 |
. . . . 5
    RRfld s   subringAlg
RRfld           RRfld s   subringAlg RRfld      ↾s     |
13 | 9, 12 | ax-mp 5 |
. . . 4
   RRfld s   subringAlg
RRfld           RRfld s   subringAlg RRfld      ↾s    |
14 | | eqid 2622 |
. . . . . 6
RRfld s   subringAlg RRfld      RRfld s   subringAlg
RRfld       |
15 | | refld 19965 |
. . . . . . 7
RRfld Field |
16 | 15 | a1i 11 |
. . . . . 6
 RRfld Field |
17 | | snex 4908 |
. . . . . . 7
  subringAlg RRfld   
 |
18 | | xpexg 6960 |
. . . . . . 7
    subringAlg
RRfld        subringAlg RRfld       |
19 | 17, 18 | mpan2 707 |
. . . . . 6
    subringAlg RRfld       |
20 | | eqid 2622 |
. . . . . 6
   RRfld s   subringAlg
RRfld          RRfld s   subringAlg
RRfld        |
21 | | fvex 6201 |
. . . . . . . . 9
 subringAlg RRfld    |
22 | 21 | snnz 4309 |
. . . . . . . 8
  subringAlg RRfld   
 |
23 | | dmxp 5344 |
. . . . . . . 8
   subringAlg
RRfld    
  subringAlg RRfld       |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
   subringAlg RRfld      |
25 | 24 | a1i 11 |
. . . . . 6
 
  subringAlg RRfld       |
26 | 14, 16, 19, 20, 25, 11 | prdsip 16121 |
. . . . 5
    RRfld s   subringAlg
RRfld           RRfld s   subringAlg RRfld           RRfld s   subringAlg
RRfld       RRfld
g               subringAlg RRfld                    |
27 | 14, 16, 19, 20, 25 | prdsbas 16117 |
. . . . . . 7
    RRfld s   subringAlg
RRfld       
       subringAlg RRfld           |
28 | | eqidd 2623 |
. . . . . . . . . . 11
  subringAlg RRfld  
 subringAlg RRfld     |
29 | | rebase 19952 |
. . . . . . . . . . . . 13
  RRfld |
30 | 29 | eqimssi 3659 |
. . . . . . . . . . . 12
  RRfld |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
   RRfld  |
32 | 28, 31 | srabase 19178 |
. . . . . . . . . 10
   RRfld     subringAlg RRfld      |
33 | 29 | a1i 11 |
. . . . . . . . . 10
   RRfld  |
34 | 21 | fvconst2 6469 |
. . . . . . . . . . 11
     subringAlg
RRfld         subringAlg RRfld     |
35 | 34 | fveq2d 6195 |
. . . . . . . . . 10
        subringAlg RRfld             subringAlg RRfld      |
36 | 32, 33, 35 | 3eqtr4rd 2667 |
. . . . . . . . 9
        subringAlg RRfld           |
37 | 36 | adantl 482 |
. . . . . . . 8
 
        subringAlg
RRfld           |
38 | 37 | ixpeq2dva 7923 |
. . . . . . 7
 
       subringAlg RRfld            |
39 | | reex 10027 |
. . . . . . . 8
 |
40 | | ixpconstg 7917 |
. . . . . . . 8
        |
41 | 39, 40 | mpan2 707 |
. . . . . . 7
 

   |
42 | 27, 38, 41 | 3eqtrd 2660 |
. . . . . 6
    RRfld s   subringAlg
RRfld           |
43 | | remulr 19957 |
. . . . . . . . . . 11
  RRfld |
44 | 34, 31 | sraip 19183 |
. . . . . . . . . . 11
   RRfld        subringAlg RRfld           |
45 | 43, 44 | syl5req 2669 |
. . . . . . . . . 10
        subringAlg RRfld          |
46 | 45 | oveqd 6667 |
. . . . . . . . 9
              subringAlg RRfld                           |
47 | 46 | mpteq2ia 4740 |
. . . . . . . 8
              subringAlg
RRfld                             |
48 | 47 | a1i 11 |
. . . . . . 7
               subringAlg RRfld                              |
49 | 48 | oveq2d 6666 |
. . . . . 6
 RRfld g               subringAlg RRfld                 RRfld g                |
50 | 42, 42, 49 | mpt2eq123dv 6717 |
. . . . 5
     RRfld s   subringAlg
RRfld           RRfld s   subringAlg RRfld       RRfld g               subringAlg RRfld                        RRfld g                 |
51 | 26, 50 | eqtrd 2656 |
. . . 4
    RRfld s   subringAlg
RRfld             RRfld g                 |
52 | 13, 51 | syl5eqr 2670 |
. . 3
     RRfld s   subringAlg RRfld      ↾s         RRfld g                 |
53 | 7, 52 | syl5eqr 2670 |
. 2
    toCHil  RRfld s   subringAlg
RRfld      ↾s          RRfld g                 |
54 | 4, 53 | eqtr2d 2657 |
1
       RRfld g                     |