Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . 3
ℝ^   |
2 | 1 | rrxval 22346 |
. 2
 toCHil RRfld freeLMod     |
3 | | eqid 2451 |
. . 3
toCHil RRfld freeLMod   toCHil RRfld freeLMod    |
4 | | eqid 2451 |
. . 3
   RRfld freeLMod      RRfld freeLMod    |
5 | | eqid 2451 |
. . 3
Scalar RRfld freeLMod   Scalar RRfld freeLMod    |
6 | | eqid 2451 |
. . . 4
RRfld freeLMod  RRfld
freeLMod   |
7 | | rebase 19174 |
. . . 4
  RRfld |
8 | | remulr 19179 |
. . . 4
  RRfld |
9 | | eqid 2451 |
. . . 4
   RRfld
freeLMod      RRfld freeLMod    |
10 | | eqid 2451 |
. . . 4
   RRfld
freeLMod      RRfld freeLMod    |
11 | | re0g 19180 |
. . . 4
  RRfld |
12 | | refldcj 19188 |
. . . 4
   RRfld |
13 | | refld 19187 |
. . . . 5
RRfld Field |
14 | 13 | a1i 11 |
. . . 4
 RRfld Field |
15 | | fconstmpt 4878 |
. . . . 5
       |
16 | 6, 7, 4 | frlmbasf 19323 |
. . . . . . . 8
 
   RRfld freeLMod          |
17 | | ffn 5728 |
. . . . . . . 8
       |
18 | 16, 17 | syl 17 |
. . . . . . 7
 
   RRfld freeLMod      |
19 | 18 | 3adant3 1028 |
. . . . . 6
 
   RRfld freeLMod        RRfld
freeLMod     
  |
20 | | simpl 459 |
. . . . . . . . . . . . . . . . 17
 
   RRfld freeLMod      |
21 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
   RRfld freeLMod    RRfld
Field |
22 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   RRfld freeLMod       RRfld freeLMod     |
23 | 6, 7, 8, 4, 9 | frlmipval 19337 |
. . . . . . . . . . . . . . . . 17
   RRfld Field     RRfld freeLMod  
   RRfld freeLMod    
     RRfld freeLMod     RRfld g       |
24 | 20, 21, 22, 22, 23 | syl22anc 1269 |
. . . . . . . . . . . . . . . 16
 
   RRfld freeLMod         RRfld freeLMod     RRfld g       |
25 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . 20
           |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
  
   RRfld
freeLMod                 |
27 | | inidm 3641 |
. . . . . . . . . . . . . . . . . . . 20
   |
28 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . 20
  
   RRfld
freeLMod               |
29 | 18, 18, 20, 20, 27, 28, 28 | offval 6538 |
. . . . . . . . . . . . . . . . . . 19
 
   RRfld freeLMod                     |
30 | 18, 18, 20, 20, 27, 28, 28 | ofval 6540 |
. . . . . . . . . . . . . . . . . . . 20
  
   RRfld
freeLMod                        |
31 | 16 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . 21
  
   RRfld
freeLMod           |
32 | 31, 31 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . 20
  
   RRfld
freeLMod                 |
33 | 30, 32 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . 19
  
   RRfld
freeLMod              |
34 | 26, 29, 33 | fmpt2d 6053 |
. . . . . . . . . . . . . . . . . 18
 
   RRfld freeLMod             |
35 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . 20
    |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
   RRfld freeLMod         |
37 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . . 20
       
     |
38 | 34, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
   RRfld freeLMod   
 
   |
39 | 6, 11, 4 | frlmbasfsupp 19321 |
. . . . . . . . . . . . . . . . . . 19
 
   RRfld freeLMod    finSupp
  |
40 | | 0red 9644 |
. . . . . . . . . . . . . . . . . . . 20
 
   RRfld freeLMod      |
41 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
  
   RRfld
freeLMod       |
42 | 41 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . 21
  
   RRfld
freeLMod       |
43 | 42 | mul02d 9831 |
. . . . . . . . . . . . . . . . . . . 20
  
   RRfld
freeLMod         |
44 | 20, 40, 16, 16, 43 | suppofss1d 6952 |
. . . . . . . . . . . . . . . . . . 19
 
   RRfld freeLMod        supp   supp
   |
45 | | fsuppsssupp 7899 |
. . . . . . . . . . . . . . . . . . 19
           finSupp     supp   supp   
 
 finSupp   |
46 | 36, 38, 39, 44, 45 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . 18
 
   RRfld freeLMod       finSupp   |
47 | | regsumsupp 19190 |
. . . . . . . . . . . . . . . . . 18
            finSupp  RRfld
g          supp            |
48 | 34, 46, 20, 47 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
 
   RRfld freeLMod    RRfld
g          supp            |
49 | | suppssdm 6927 |
. . . . . . . . . . . . . . . . . . . . . 22
 supp   |
50 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
51 | 16, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   RRfld freeLMod   
  |
52 | 49, 51 | syl5sseq 3480 |
. . . . . . . . . . . . . . . . . . . . 21
 
   RRfld freeLMod     supp 
  |
53 | 44, 52 | sstrd 3442 |
. . . . . . . . . . . . . . . . . . . 20
 
   RRfld freeLMod        supp    |
54 | 53 | sselda 3432 |
. . . . . . . . . . . . . . . . . . 19
  
   RRfld
freeLMod        supp  
  |
55 | 54, 30 | syldan 473 |
. . . . . . . . . . . . . . . . . 18
  
   RRfld
freeLMod        supp                      |
56 | 55 | sumeq2dv 13769 |
. . . . . . . . . . . . . . . . 17
 
   RRfld freeLMod         supp               supp               |
57 | 48, 56 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
 
   RRfld freeLMod    RRfld
g          supp               |
58 | 24, 57 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
 
   RRfld freeLMod         RRfld freeLMod     
    supp               |
59 | 58 | 3adant3 1028 |
. . . . . . . . . . . . . 14
 
   RRfld freeLMod        RRfld
freeLMod     
     RRfld freeLMod          supp               |
60 | | simp3 1010 |
. . . . . . . . . . . . . 14
 
   RRfld freeLMod        RRfld
freeLMod     
     RRfld freeLMod       |
61 | 59, 60 | eqtr3d 2487 |
. . . . . . . . . . . . 13
 
   RRfld freeLMod        RRfld
freeLMod     
     supp               |
62 | 39 | fsuppimpd 7890 |
. . . . . . . . . . . . . . . 16
 
   RRfld freeLMod     supp    |
63 | | ssfi 7792 |
. . . . . . . . . . . . . . . 16
   supp      supp 
 supp       supp    |
64 | 62, 44, 63 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
   RRfld freeLMod        supp    |
65 | 54, 32 | syldan 473 |
. . . . . . . . . . . . . . 15
  
   RRfld
freeLMod        supp               |
66 | 31 | msqge0d 10182 |
. . . . . . . . . . . . . . . 16
  
   RRfld
freeLMod                 |
67 | 54, 66 | syldan 473 |
. . . . . . . . . . . . . . 15
  
   RRfld
freeLMod        supp  
            |
68 | 64, 65, 67 | fsum00 13858 |
. . . . . . . . . . . . . 14
 
   RRfld freeLMod          supp                  supp                |
69 | 68 | 3adant3 1028 |
. . . . . . . . . . . . 13
 
   RRfld freeLMod        RRfld
freeLMod     
      supp            
     supp                |
70 | 61, 69 | mpbid 214 |
. . . . . . . . . . . 12
 
   RRfld freeLMod        RRfld
freeLMod     
     supp               |
71 | 70 | r19.21bi 2757 |
. . . . . . . . . . 11
  
   RRfld
freeLMod        RRfld freeLMod          supp               |
72 | 71 | adantlr 721 |
. . . . . . . . . 10
       RRfld freeLMod        RRfld freeLMod      
    supp               |
73 | 31 | 3adantl3 1166 |
. . . . . . . . . . . . 13
  
   RRfld
freeLMod        RRfld freeLMod             |
74 | 73 | recnd 9669 |
. . . . . . . . . . . 12
  
   RRfld
freeLMod        RRfld freeLMod             |
75 | 74, 74 | mul0ord 10262 |
. . . . . . . . . . 11
  
   RRfld
freeLMod        RRfld freeLMod                               |
76 | 75 | adantr 467 |
. . . . . . . . . 10
       RRfld freeLMod        RRfld freeLMod      
    supp                           |
77 | 72, 76 | mpbid 214 |
. . . . . . . . 9
       RRfld freeLMod        RRfld freeLMod      
    supp               |
78 | | oridm 517 |
. . . . . . . . 9
                 |
79 | 77, 78 | sylib 200 |
. . . . . . . 8
       RRfld freeLMod        RRfld freeLMod      
    supp         |
80 | 34 | 3adant3 1028 |
. . . . . . . . . . 11
 
   RRfld freeLMod        RRfld
freeLMod     
 
       |
81 | 80 | adantr 467 |
. . . . . . . . . 10
  
   RRfld
freeLMod        RRfld freeLMod                |
82 | | ssid 3451 |
. . . . . . . . . . 11
    supp      supp   |
83 | 82 | a1i 11 |
. . . . . . . . . 10
  
   RRfld
freeLMod        RRfld freeLMod           supp 
    supp    |
84 | | simpl1 1011 |
. . . . . . . . . 10
  
   RRfld
freeLMod        RRfld freeLMod         |
85 | | 0red 9644 |
. . . . . . . . . 10
  
   RRfld
freeLMod        RRfld freeLMod         |
86 | 81, 83, 84, 85 | suppssr 6946 |
. . . . . . . . 9
       RRfld freeLMod        RRfld freeLMod      

    supp             |
87 | 30 | 3adantl3 1166 |
. . . . . . . . . . . . 13
  
   RRfld
freeLMod        RRfld freeLMod                          |
88 | 87 | eqeq1d 2453 |
. . . . . . . . . . . 12
  
   RRfld
freeLMod        RRfld freeLMod                            |
89 | 88, 75 | bitrd 257 |
. . . . . . . . . . 11
  
   RRfld
freeLMod        RRfld freeLMod                            |
90 | 89, 78 | syl6bb 265 |
. . . . . . . . . 10
  
   RRfld
freeLMod        RRfld freeLMod                      |
91 | 90 | biimpa 487 |
. . . . . . . . 9
       RRfld freeLMod        RRfld freeLMod      
              |
92 | 86, 91 | syldan 473 |
. . . . . . . 8
       RRfld freeLMod        RRfld freeLMod      

    supp          |
93 | | undif 3848 |
. . . . . . . . . . . . 13
     supp 
     supp       supp      |
94 | 53, 93 | sylib 200 |
. . . . . . . . . . . 12
 
   RRfld freeLMod         supp       supp      |
95 | 94 | eleq2d 2514 |
. . . . . . . . . . 11
 
   RRfld freeLMod          supp       supp   
   |
96 | 95 | 3adant3 1028 |
. . . . . . . . . 10
 
   RRfld freeLMod        RRfld
freeLMod     
      supp       supp   
   |
97 | 96 | biimpar 488 |
. . . . . . . . 9
  
   RRfld
freeLMod        RRfld freeLMod            supp       supp      |
98 | | elun 3574 |
. . . . . . . . 9
      supp       supp         supp       supp      |
99 | 97, 98 | sylib 200 |
. . . . . . . 8
  
   RRfld
freeLMod        RRfld freeLMod            supp       supp      |
100 | 79, 92, 99 | mpjaodan 795 |
. . . . . . 7
  
   RRfld
freeLMod        RRfld freeLMod             |
101 | 100 | ralrimiva 2802 |
. . . . . 6
 
   RRfld freeLMod        RRfld
freeLMod     

      |
102 | | fconstfv 6126 |
. . . . . . . 8
        
       |
103 | 102 | biimpri 210 |
. . . . . . 7
                |
104 | | c0ex 9637 |
. . . . . . . 8
 |
105 | 104 | fconst2 6121 |
. . . . . . 7
             |
106 | 103, 105 | sylib 200 |
. . . . . 6
              |
107 | 19, 101, 106 | syl2anc 667 |
. . . . 5
 
   RRfld freeLMod        RRfld
freeLMod     

     |
108 | | isfld 17984 |
. . . . . . . . . . 11
RRfld Field RRfld
RRfld    |
109 | 13, 108 | mpbi 212 |
. . . . . . . . . 10
RRfld RRfld   |
110 | 109 | simpli 460 |
. . . . . . . . 9
RRfld  |
111 | | drngring 17982 |
. . . . . . . . 9
RRfld RRfld   |
112 | 110, 111 | ax-mp 5 |
. . . . . . . 8
RRfld  |
113 | 6, 11 | frlm0 19317 |
. . . . . . . 8
 RRfld
        RRfld freeLMod     |
114 | 112, 113 | mpan 676 |
. . . . . . 7
        RRfld freeLMod     |
115 | 15, 114 | syl5reqr 2500 |
. . . . . 6
    RRfld
freeLMod       |
116 | 115 | 3ad2ant1 1029 |
. . . . 5
 
   RRfld freeLMod        RRfld
freeLMod     
   RRfld freeLMod       |
117 | 15, 107, 116 | 3eqtr4a 2511 |
. . . 4
 
   RRfld freeLMod        RRfld
freeLMod     
   RRfld freeLMod     |
118 | | cjre 13202 |
. . . . 5
       |
119 | 118 | adantl 468 |
. . . 4
 
       |
120 | | id 22 |
. . . 4
   |
121 | 6, 7, 8, 4, 9, 10,
11, 12, 14, 117, 119, 120 | frlmphl 19339 |
. . 3
 RRfld freeLMod    |
122 | | df-refld 19173 |
. . . 4
RRfld ℂfld ↾s   |
123 | 6 | frlmsca 19316 |
. . . . 5
 RRfld Field 
RRfld Scalar RRfld freeLMod     |
124 | 13, 123 | mpan 676 |
. . . 4
 RRfld Scalar RRfld freeLMod     |
125 | 122, 124 | syl5reqr 2500 |
. . 3
 Scalar RRfld freeLMod   ℂfld ↾s    |
126 | | simpr1 1014 |
. . . 4
       |
127 | | simpr3 1016 |
. . . 4
       |
128 | 126, 127 | resqrtcld 13479 |
. . 3
           |
129 | 64, 65, 67 | fsumge0 13855 |
. . . . 5
 
   RRfld freeLMod         supp               |
130 | 129, 57 | breqtrrd 4429 |
. . . 4
 
   RRfld freeLMod    RRfld g       |
131 | 130, 24 | breqtrrd 4429 |
. . 3
 
   RRfld freeLMod         RRfld freeLMod       |
132 | 3, 4, 5, 121, 125, 9, 128, 131 | tchcph 22211 |
. 2
 toCHil RRfld freeLMod     |
133 | 2, 132 | eqeltrd 2529 |
1
   |