| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdadd.s |  | 
						
							| 2 |  | psdadd.b |  | 
						
							| 3 |  | psdadd.p |  | 
						
							| 4 |  | psdadd.r |  | 
						
							| 5 |  | psdadd.x |  | 
						
							| 6 |  | psdadd.f |  | 
						
							| 7 |  | psdadd.g |  | 
						
							| 8 |  | eqid |  | 
						
							| 9 | 1 2 8 5 6 | psdval |  | 
						
							| 10 | 1 2 8 5 7 | psdval |  | 
						
							| 11 | 9 10 | oveq12d |  | 
						
							| 12 |  | ovex |  | 
						
							| 13 |  | eqid |  | 
						
							| 14 | 12 13 | fnmpti |  | 
						
							| 15 | 14 | a1i |  | 
						
							| 16 |  | ovex |  | 
						
							| 17 |  | eqid |  | 
						
							| 18 | 16 17 | fnmpti |  | 
						
							| 19 | 18 | a1i |  | 
						
							| 20 |  | ovex |  | 
						
							| 21 | 20 | rabex |  | 
						
							| 22 | 21 | a1i |  | 
						
							| 23 |  | inidm |  | 
						
							| 24 |  | fveq1 |  | 
						
							| 25 | 24 | oveq1d |  | 
						
							| 26 |  | fvoveq1 |  | 
						
							| 27 | 25 26 | oveq12d |  | 
						
							| 28 |  | simpr |  | 
						
							| 29 |  | ovexd |  | 
						
							| 30 | 13 27 28 29 | fvmptd3 |  | 
						
							| 31 |  | fvoveq1 |  | 
						
							| 32 | 25 31 | oveq12d |  | 
						
							| 33 |  | ovexd |  | 
						
							| 34 | 17 32 28 33 | fvmptd3 |  | 
						
							| 35 | 15 19 22 22 23 30 34 | offval |  | 
						
							| 36 |  | eqid |  | 
						
							| 37 | 1 2 36 3 6 7 | psradd |  | 
						
							| 38 | 37 | adantr |  | 
						
							| 39 | 38 | fveq1d |  | 
						
							| 40 |  | reldmpsr |  | 
						
							| 41 | 1 2 40 | strov2rcl |  | 
						
							| 42 | 6 41 | syl |  | 
						
							| 43 | 8 | psrbagsn |  | 
						
							| 44 | 42 43 | syl |  | 
						
							| 45 | 44 | adantr |  | 
						
							| 46 | 8 | psrbagaddcl |  | 
						
							| 47 | 28 45 46 | syl2anc |  | 
						
							| 48 |  | eqid |  | 
						
							| 49 | 1 48 8 2 6 | psrelbas |  | 
						
							| 50 | 49 | ffnd |  | 
						
							| 51 | 1 48 8 2 7 | psrelbas |  | 
						
							| 52 | 51 | ffnd |  | 
						
							| 53 |  | eqidd |  | 
						
							| 54 |  | eqidd |  | 
						
							| 55 | 50 52 22 22 23 53 54 | ofval |  | 
						
							| 56 | 47 55 | syldan |  | 
						
							| 57 | 39 56 | eqtrd |  | 
						
							| 58 | 57 | oveq2d |  | 
						
							| 59 | 4 | adantr |  | 
						
							| 60 | 8 | psrbagf |  | 
						
							| 61 | 60 | adantl |  | 
						
							| 62 | 5 | adantr |  | 
						
							| 63 | 61 62 | ffvelcdmd |  | 
						
							| 64 |  | peano2nn0 |  | 
						
							| 65 | 63 64 | syl |  | 
						
							| 66 | 6 | adantr |  | 
						
							| 67 | 1 48 8 2 66 | psrelbas |  | 
						
							| 68 | 67 47 | ffvelcdmd |  | 
						
							| 69 | 51 | adantr |  | 
						
							| 70 | 69 47 | ffvelcdmd |  | 
						
							| 71 |  | eqid |  | 
						
							| 72 | 48 71 36 | mulgnn0di |  | 
						
							| 73 | 59 65 68 70 72 | syl13anc |  | 
						
							| 74 | 58 73 | eqtr2d |  | 
						
							| 75 | 74 | mpteq2dva |  | 
						
							| 76 | 11 35 75 | 3eqtrd |  | 
						
							| 77 | 4 | cmnmndd |  | 
						
							| 78 |  | mndmgm |  | 
						
							| 79 | 77 78 | syl |  | 
						
							| 80 | 1 2 79 5 6 | psdcl |  | 
						
							| 81 | 1 2 79 5 7 | psdcl |  | 
						
							| 82 | 1 2 36 3 80 81 | psradd |  | 
						
							| 83 | 1 2 3 79 6 7 | psraddcl |  | 
						
							| 84 | 1 2 8 5 83 | psdval |  | 
						
							| 85 | 76 82 84 | 3eqtr4rd |  |