| Step | Hyp | Ref | Expression | 
						
							| 1 |  | dfufd2.b | ⊢ 𝐵  =  ( Base ‘ 𝑅 ) | 
						
							| 2 |  | dfufd2.0 | ⊢  0   =  ( 0g ‘ 𝑅 ) | 
						
							| 3 |  | dfufd2.u | ⊢ 𝑈  =  ( Unit ‘ 𝑅 ) | 
						
							| 4 |  | dfufd2.p | ⊢ 𝑃  =  ( RPrime ‘ 𝑅 ) | 
						
							| 5 |  | dfufd2.m | ⊢ 𝑀  =  ( mulGrp ‘ 𝑅 ) | 
						
							| 6 |  | id | ⊢ ( 𝑅  ∈  UFD  →  𝑅  ∈  UFD ) | 
						
							| 7 | 6 | ufdidom | ⊢ ( 𝑅  ∈  UFD  →  𝑅  ∈  IDomn ) | 
						
							| 8 |  | simpl | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  𝑅  ∈  UFD ) | 
						
							| 9 |  | simpr | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ) | 
						
							| 10 | 9 | eldifad | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  𝑥  ∈  ( 𝐵  ∖  𝑈 ) ) | 
						
							| 11 | 10 | eldifad | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  𝑥  ∈  𝐵 ) | 
						
							| 12 | 10 | eldifbd | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  ¬  𝑥  ∈  𝑈 ) | 
						
							| 13 |  | eldifsni | ⊢ ( 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } )  →  𝑥  ≠   0  ) | 
						
							| 14 | 13 | adantl | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  𝑥  ≠   0  ) | 
						
							| 15 | 1 2 3 4 5 8 11 12 14 | 1arithufd | ⊢ ( ( 𝑅  ∈  UFD  ∧  𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) )  →  ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) ) | 
						
							| 16 | 15 | ralrimiva | ⊢ ( 𝑅  ∈  UFD  →  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) ) | 
						
							| 17 | 7 16 | jca | ⊢ ( 𝑅  ∈  UFD  →  ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) ) ) | 
						
							| 18 |  | simpl | ⊢ ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  →  𝑅  ∈  IDomn ) | 
						
							| 19 |  | id | ⊢ ( 𝑅  ∈  IDomn  →  𝑅  ∈  IDomn ) | 
						
							| 20 | 19 | idomringd | ⊢ ( 𝑅  ∈  IDomn  →  𝑅  ∈  Ring ) | 
						
							| 21 | 20 | ad2antrr | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑅  ∈  Ring ) | 
						
							| 22 |  | simpr | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) ) | 
						
							| 23 | 22 | eldifad | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ∈  ( PrmIdeal ‘ 𝑅 ) ) | 
						
							| 24 |  | prmidlidl | ⊢ ( ( 𝑅  ∈  Ring  ∧  𝑖  ∈  ( PrmIdeal ‘ 𝑅 ) )  →  𝑖  ∈  ( LIdeal ‘ 𝑅 ) ) | 
						
							| 25 | 21 23 24 | syl2anc | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ∈  ( LIdeal ‘ 𝑅 ) ) | 
						
							| 26 |  | eqid | ⊢ ( LIdeal ‘ 𝑅 )  =  ( LIdeal ‘ 𝑅 ) | 
						
							| 27 | 1 26 | lidlss | ⊢ ( 𝑖  ∈  ( LIdeal ‘ 𝑅 )  →  𝑖  ⊆  𝐵 ) | 
						
							| 28 | 25 27 | syl | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ⊆  𝐵 ) | 
						
							| 29 | 28 | sselda | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  𝑦  ∈  𝐵 ) | 
						
							| 30 |  | simpr | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  𝑦  ∈  𝑈 ) | 
						
							| 31 |  | simplr | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  𝑦  ∈  𝑖 ) | 
						
							| 32 | 21 | ad2antrr | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  𝑅  ∈  Ring ) | 
						
							| 33 | 25 | ad2antrr | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  𝑖  ∈  ( LIdeal ‘ 𝑅 ) ) | 
						
							| 34 | 1 3 30 31 32 33 | lidlunitel | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  𝑖  =  𝐵 ) | 
						
							| 35 |  | eqid | ⊢ ( .r ‘ 𝑅 )  =  ( .r ‘ 𝑅 ) | 
						
							| 36 | 1 35 | prmidlnr | ⊢ ( ( 𝑅  ∈  Ring  ∧  𝑖  ∈  ( PrmIdeal ‘ 𝑅 ) )  →  𝑖  ≠  𝐵 ) | 
						
							| 37 | 21 23 36 | syl2anc | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ≠  𝐵 ) | 
						
							| 38 | 37 | ad2antrr | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  𝑖  ≠  𝐵 ) | 
						
							| 39 | 38 | neneqd | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ∈  𝑈 )  →  ¬  𝑖  =  𝐵 ) | 
						
							| 40 | 34 39 | pm2.65da | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  ¬  𝑦  ∈  𝑈 ) | 
						
							| 41 | 29 40 | eldifd | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  𝑦  ∈  ( 𝐵  ∖  𝑈 ) ) | 
						
							| 42 |  | simpllr | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  𝑦  ≠   0  ) | 
						
							| 43 | 41 42 | eldifsnd | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  𝑦  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ) | 
						
							| 44 |  | eqeq1 | ⊢ ( 𝑥  =  𝑦  →  ( 𝑥  =  ( 𝑀  Σg  𝑓 )  ↔  𝑦  =  ( 𝑀  Σg  𝑓 ) ) ) | 
						
							| 45 | 44 | rexbidv | ⊢ ( 𝑥  =  𝑦  →  ( ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 )  ↔  ∃ 𝑓  ∈  Word  𝑃 𝑦  =  ( 𝑀  Σg  𝑓 ) ) ) | 
						
							| 46 | 45 | adantl | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑥  =  𝑦 )  →  ( ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 )  ↔  ∃ 𝑓  ∈  Word  𝑃 𝑦  =  ( 𝑀  Σg  𝑓 ) ) ) | 
						
							| 47 | 43 46 | rspcdv | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  ( ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 )  →  ∃ 𝑓  ∈  Word  𝑃 𝑦  =  ( 𝑀  Σg  𝑓 ) ) ) | 
						
							| 48 |  | simp-5l | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  𝑅  ∈  IDomn ) | 
						
							| 49 | 23 | ad3antrrr | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  𝑖  ∈  ( PrmIdeal ‘ 𝑅 ) ) | 
						
							| 50 |  | simplr | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  𝑓  ∈  Word  𝑃 ) | 
						
							| 51 |  | simpr | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  𝑦  =  ( 𝑀  Σg  𝑓 ) ) | 
						
							| 52 |  | simpllr | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  𝑦  ∈  𝑖 ) | 
						
							| 53 | 51 52 | eqeltrrd | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  ( 𝑀  Σg  𝑓 )  ∈  𝑖 ) | 
						
							| 54 | 42 | ad2antrr | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  𝑦  ≠   0  ) | 
						
							| 55 | 51 54 | eqnetrrd | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  ( 𝑀  Σg  𝑓 )  ≠   0  ) | 
						
							| 56 | 1 2 3 4 5 48 49 50 53 55 | dfufd2lem | ⊢ ( ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑓  ∈  Word  𝑃 )  ∧  𝑦  =  ( 𝑀  Σg  𝑓 ) )  →  ( 𝑖  ∩  𝑃 )  ≠  ∅ ) | 
						
							| 57 | 56 | rexlimdva2 | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  ( ∃ 𝑓  ∈  Word  𝑃 𝑦  =  ( 𝑀  Σg  𝑓 )  →  ( 𝑖  ∩  𝑃 )  ≠  ∅ ) ) | 
						
							| 58 | 47 57 | syld | ⊢ ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  →  ( ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 )  →  ( 𝑖  ∩  𝑃 )  ≠  ∅ ) ) | 
						
							| 59 | 58 | imp | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  𝑦  ≠   0  )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  →  ( 𝑖  ∩  𝑃 )  ≠  ∅ ) | 
						
							| 60 | 59 | an52ds | ⊢ ( ( ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  ∧  𝑦  ∈  𝑖 )  ∧  𝑦  ≠   0  )  →  ( 𝑖  ∩  𝑃 )  ≠  ∅ ) | 
						
							| 61 | 20 | ad2antrr | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑅  ∈  Ring ) | 
						
							| 62 |  | simpr | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) ) | 
						
							| 63 | 62 | eldifad | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ∈  ( PrmIdeal ‘ 𝑅 ) ) | 
						
							| 64 | 61 63 24 | syl2anc | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ∈  ( LIdeal ‘ 𝑅 ) ) | 
						
							| 65 |  | eldifsni | ⊢ ( 𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } )  →  𝑖  ≠  {  0  } ) | 
						
							| 66 | 65 | adantl | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  𝑖  ≠  {  0  } ) | 
						
							| 67 | 26 2 | lidlnz | ⊢ ( ( 𝑅  ∈  Ring  ∧  𝑖  ∈  ( LIdeal ‘ 𝑅 )  ∧  𝑖  ≠  {  0  } )  →  ∃ 𝑦  ∈  𝑖 𝑦  ≠   0  ) | 
						
							| 68 | 61 64 66 67 | syl3anc | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  ∃ 𝑦  ∈  𝑖 𝑦  ≠   0  ) | 
						
							| 69 | 60 68 | r19.29a | ⊢ ( ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  ∧  𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) )  →  ( 𝑖  ∩  𝑃 )  ≠  ∅ ) | 
						
							| 70 | 69 | ralrimiva | ⊢ ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  →  ∀ 𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) ( 𝑖  ∩  𝑃 )  ≠  ∅ ) | 
						
							| 71 |  | eqid | ⊢ ( PrmIdeal ‘ 𝑅 )  =  ( PrmIdeal ‘ 𝑅 ) | 
						
							| 72 | 71 4 2 | isufd | ⊢ ( 𝑅  ∈  UFD  ↔  ( 𝑅  ∈  IDomn  ∧  ∀ 𝑖  ∈  ( ( PrmIdeal ‘ 𝑅 )  ∖  { {  0  } } ) ( 𝑖  ∩  𝑃 )  ≠  ∅ ) ) | 
						
							| 73 | 18 70 72 | sylanbrc | ⊢ ( ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) )  →  𝑅  ∈  UFD ) | 
						
							| 74 | 17 73 | impbii | ⊢ ( 𝑅  ∈  UFD  ↔  ( 𝑅  ∈  IDomn  ∧  ∀ 𝑥  ∈  ( ( 𝐵  ∖  𝑈 )  ∖  {  0  } ) ∃ 𝑓  ∈  Word  𝑃 𝑥  =  ( 𝑀  Σg  𝑓 ) ) ) |