| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdmplcl.p |  | 
						
							| 2 |  | psdmplcl.b |  | 
						
							| 3 |  | psdmplcl.r |  | 
						
							| 4 |  | psdmplcl.x |  | 
						
							| 5 |  | psdmplcl.f |  | 
						
							| 6 |  | eqid |  | 
						
							| 7 |  | eqid |  | 
						
							| 8 |  | mndmgm |  | 
						
							| 9 | 3 8 | syl |  | 
						
							| 10 | 1 6 2 7 | mplbasss |  | 
						
							| 11 | 10 5 | sselid |  | 
						
							| 12 | 6 7 9 4 11 | psdcl |  | 
						
							| 13 |  | eqid |  | 
						
							| 14 | 6 7 13 4 11 | psdval |  | 
						
							| 15 |  | ovex |  | 
						
							| 16 | 15 | rabex |  | 
						
							| 17 | 16 | a1i |  | 
						
							| 18 | 17 | mptexd |  | 
						
							| 19 |  | fvexd |  | 
						
							| 20 |  | funmpt |  | 
						
							| 21 | 20 | a1i |  | 
						
							| 22 |  | simpr |  | 
						
							| 23 |  | reldmmpl |  | 
						
							| 24 | 1 2 23 | strov2rcl |  | 
						
							| 25 | 5 24 | syl |  | 
						
							| 26 | 13 | psrbagsn |  | 
						
							| 27 | 25 26 | syl |  | 
						
							| 28 | 27 | adantr |  | 
						
							| 29 | 13 | psrbagaddcl |  | 
						
							| 30 | 22 28 29 | syl2anc |  | 
						
							| 31 |  | eqidd |  | 
						
							| 32 |  | eqid |  | 
						
							| 33 | 1 32 2 13 5 | mplelf |  | 
						
							| 34 | 33 | feqmptd |  | 
						
							| 35 |  | fveq2 |  | 
						
							| 36 | 30 31 34 35 | fmptco |  | 
						
							| 37 |  | eqid |  | 
						
							| 38 | 1 2 37 5 | mplelsfi |  | 
						
							| 39 | 30 | fmpttd |  | 
						
							| 40 |  | ovex |  | 
						
							| 41 |  | eqid |  | 
						
							| 42 | 40 41 | fnmpti |  | 
						
							| 43 | 42 | a1i |  | 
						
							| 44 |  | dffn3 |  | 
						
							| 45 | 43 44 | sylib |  | 
						
							| 46 | 45 39 | fcod |  | 
						
							| 47 | 46 | ffnd |  | 
						
							| 48 |  | fnresi |  | 
						
							| 49 | 48 | a1i |  | 
						
							| 50 | 13 | psrbagf |  | 
						
							| 51 | 50 | adantl |  | 
						
							| 52 | 51 | ffvelcdmda |  | 
						
							| 53 | 52 | nn0cnd |  | 
						
							| 54 |  | ax-1cn |  | 
						
							| 55 |  | 0cn |  | 
						
							| 56 | 54 55 | ifcli |  | 
						
							| 57 | 56 | a1i |  | 
						
							| 58 | 53 57 | pncand |  | 
						
							| 59 | 58 | mpteq2dva |  | 
						
							| 60 |  | simpr |  | 
						
							| 61 | 27 | adantr |  | 
						
							| 62 | 13 | psrbagaddcl |  | 
						
							| 63 | 60 61 62 | syl2anc |  | 
						
							| 64 | 13 | psrbagf |  | 
						
							| 65 | 64 | ffnd |  | 
						
							| 66 | 63 65 | syl |  | 
						
							| 67 |  | 1ex |  | 
						
							| 68 |  | c0ex |  | 
						
							| 69 | 67 68 | ifex |  | 
						
							| 70 |  | eqid |  | 
						
							| 71 | 69 70 | fnmpti |  | 
						
							| 72 | 71 | a1i |  | 
						
							| 73 | 25 | adantr |  | 
						
							| 74 |  | inidm |  | 
						
							| 75 | 50 | ffnd |  | 
						
							| 76 | 75 | adantl |  | 
						
							| 77 |  | eqidd |  | 
						
							| 78 |  | eqeq1 |  | 
						
							| 79 | 78 | ifbid |  | 
						
							| 80 |  | simpr |  | 
						
							| 81 | 67 68 | ifex |  | 
						
							| 82 | 81 | a1i |  | 
						
							| 83 | 70 79 80 82 | fvmptd3 |  | 
						
							| 84 | 76 72 73 73 74 77 83 | ofval |  | 
						
							| 85 | 66 72 73 73 74 84 83 | offval |  | 
						
							| 86 | 51 | feqmptd |  | 
						
							| 87 | 59 85 86 | 3eqtr4d |  | 
						
							| 88 | 30 | adantlr |  | 
						
							| 89 | 88 | fmpttd |  | 
						
							| 90 | 89 60 | fvco3d |  | 
						
							| 91 |  | eqid |  | 
						
							| 92 |  | oveq1 |  | 
						
							| 93 |  | ovexd |  | 
						
							| 94 | 91 92 60 93 | fvmptd3 |  | 
						
							| 95 | 94 | fveq2d |  | 
						
							| 96 |  | oveq1 |  | 
						
							| 97 |  | ovexd |  | 
						
							| 98 | 41 96 63 97 | fvmptd3 |  | 
						
							| 99 | 90 95 98 | 3eqtrd |  | 
						
							| 100 |  | fvresi |  | 
						
							| 101 | 100 | adantl |  | 
						
							| 102 | 87 99 101 | 3eqtr4d |  | 
						
							| 103 | 47 49 102 | eqfnfvd |  | 
						
							| 104 |  | fcof1 |  | 
						
							| 105 | 39 103 104 | syl2anc |  | 
						
							| 106 | 38 105 19 5 | fsuppco |  | 
						
							| 107 | 36 106 | eqbrtrrd |  | 
						
							| 108 | 107 | fsuppimpd |  | 
						
							| 109 |  | ssidd |  | 
						
							| 110 |  | eqid |  | 
						
							| 111 | 32 110 37 | mulgnn0z |  | 
						
							| 112 | 3 111 | sylan |  | 
						
							| 113 | 13 | psrbagf |  | 
						
							| 114 | 113 | adantl |  | 
						
							| 115 | 4 | adantr |  | 
						
							| 116 | 114 115 | ffvelcdmd |  | 
						
							| 117 |  | peano2nn0 |  | 
						
							| 118 | 116 117 | syl |  | 
						
							| 119 |  | fvexd |  | 
						
							| 120 | 109 112 118 119 19 | suppssov2 |  | 
						
							| 121 | 108 120 | ssfid |  | 
						
							| 122 | 18 19 21 121 | isfsuppd |  | 
						
							| 123 | 14 122 | eqbrtrd |  | 
						
							| 124 | 1 6 7 37 2 | mplelbas |  | 
						
							| 125 | 12 123 124 | sylanbrc |  |