| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqeq1 2740 | . . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑥 = (𝑀 Σg 𝑓) ↔ 𝑎 = (𝑀 Σg 𝑓))) | 
| 2 | 1 | rexbidv 3178 | . . . . . . . 8
⊢ (𝑥 = 𝑎 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑎 = (𝑀 Σg 𝑓))) | 
| 3 |  | eqcom 2743 | . . . . . . . . 9
⊢ (𝑎 = (𝑀 Σg 𝑓) ↔ (𝑀 Σg 𝑓) = 𝑎) | 
| 4 | 3 | rexbii 3093 | . . . . . . . 8
⊢
(∃𝑓 ∈
Word 𝑃𝑎 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑀 Σg 𝑓) = 𝑎) | 
| 5 | 2, 4 | bitrdi 287 | . . . . . . 7
⊢ (𝑥 = 𝑎 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑀 Σg 𝑓) = 𝑎)) | 
| 6 |  | 1arithufd.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) | 
| 7 |  | 1arithufd.p | . . . . . . . 8
⊢ 𝑃 = (RPrime‘𝑅) | 
| 8 |  | 1arithufd.r | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ UFD) | 
| 9 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝑅 ∈ UFD) | 
| 10 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝑎 ∈ 𝑃) | 
| 11 | 6, 7, 9, 10 | rprmcl 33547 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝑎 ∈ 𝐵) | 
| 12 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑓 = 〈“𝑎”〉 → (𝑀 Σg
𝑓) = (𝑀 Σg
〈“𝑎”〉)) | 
| 13 | 12 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑓 = 〈“𝑎”〉 → ((𝑀 Σg
𝑓) = 𝑎 ↔ (𝑀 Σg
〈“𝑎”〉) = 𝑎)) | 
| 14 | 10 | s1cld 14642 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 〈“𝑎”〉 ∈ Word 𝑃) | 
| 15 |  | 1arithufd.m | . . . . . . . . . . 11
⊢ 𝑀 = (mulGrp‘𝑅) | 
| 16 | 15, 6 | mgpbas 20143 | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑀) | 
| 17 | 16 | gsumws1 18852 | . . . . . . . . 9
⊢ (𝑎 ∈ 𝐵 → (𝑀 Σg
〈“𝑎”〉) = 𝑎) | 
| 18 | 11, 17 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → (𝑀 Σg
〈“𝑎”〉) = 𝑎) | 
| 19 | 13, 14, 18 | rspcedvdw 3624 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → ∃𝑓 ∈ Word 𝑃(𝑀 Σg 𝑓) = 𝑎) | 
| 20 | 5, 11, 19 | elrabd 3693 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝑎 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}) | 
| 21 |  | 1arithufdlem.s | . . . . . 6
⊢ 𝑆 = {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)} | 
| 22 | 20, 21 | eleqtrrdi 2851 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑃) → 𝑎 ∈ 𝑆) | 
| 23 | 22 | ex 412 | . . . 4
⊢ (𝜑 → (𝑎 ∈ 𝑃 → 𝑎 ∈ 𝑆)) | 
| 24 | 23 | ssrdv 3988 | . . 3
⊢ (𝜑 → 𝑃 ⊆ 𝑆) | 
| 25 | 24 | adantr 480 | . 2
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → 𝑃 ⊆ 𝑆) | 
| 26 |  | anass 468 | . . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ↔ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)))) | 
| 27 |  | ineq2 4213 | . . . . . . . . . . 11
⊢ (𝑝 = 𝑖 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑖)) | 
| 28 | 27 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑝 = 𝑖 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑖) = ∅)) | 
| 29 |  | sseq2 4009 | . . . . . . . . . 10
⊢ (𝑝 = 𝑖 → (((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝 ↔ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) | 
| 30 | 28, 29 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑝 = 𝑖 → (((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖))) | 
| 31 | 30 | elrab 3691 | . . . . . . . 8
⊢ (𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ↔ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖))) | 
| 32 | 31 | anbi2i 623 | . . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)}) ↔ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ (𝑖 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)))) | 
| 33 | 26, 32 | bitr4i 278 | . . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ↔ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)})) | 
| 34 | 33 | anbi1i 624 | . . . . 5
⊢
(((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ↔ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)}) ∧ 𝑖 ∈ (PrmIdeal‘𝑅))) | 
| 35 |  | incom 4208 | . . . . . . 7
⊢ (𝑖 ∩ 𝑆) = (𝑆 ∩ 𝑖) | 
| 36 |  | simpllr 775 | . . . . . . . 8
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) | 
| 37 | 36 | simpld 494 | . . . . . . 7
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → (𝑆 ∩ 𝑖) = ∅) | 
| 38 | 35, 37 | eqtrid 2788 | . . . . . 6
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → (𝑖 ∩ 𝑆) = ∅) | 
| 39 | 8 | ad5antr 734 | . . . . . . 7
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → 𝑅 ∈ UFD) | 
| 40 |  | simplr 768 | . . . . . . . 8
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ (PrmIdeal‘𝑅)) | 
| 41 | 36 | simprd 495 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖) | 
| 42 | 8 | ufdidom 33571 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ IDomn) | 
| 43 | 42 | idomringd 20729 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 44 |  | 1arithufdlem.3 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 45 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(RSpan‘𝑅) =
(RSpan‘𝑅) | 
| 46 | 6, 45 | rspsnid 33400 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ ((RSpan‘𝑅)‘{𝑋})) | 
| 47 | 43, 44, 46 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ((RSpan‘𝑅)‘{𝑋})) | 
| 48 | 47 | ad5antr 734 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → 𝑋 ∈ ((RSpan‘𝑅)‘{𝑋})) | 
| 49 | 41, 48 | sseldd 3983 | . . . . . . . . 9
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → 𝑋 ∈ 𝑖) | 
| 50 |  | 1arithufdlem.5 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≠ 0 ) | 
| 51 |  | nelsn 4665 | . . . . . . . . . . 11
⊢ (𝑋 ≠ 0 → ¬ 𝑋 ∈ { 0 }) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ { 0 }) | 
| 53 | 52 | ad5antr 734 | . . . . . . . . 9
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → ¬ 𝑋 ∈ { 0 }) | 
| 54 |  | nelne1 3038 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑖 ∧ ¬ 𝑋 ∈ { 0 }) → 𝑖 ≠ { 0 }) | 
| 55 | 49, 53, 54 | syl2anc 584 | . . . . . . . 8
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → 𝑖 ≠ { 0 }) | 
| 56 | 40, 55 | eldifsnd 4786 | . . . . . . 7
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) | 
| 57 |  | ineq1 4212 | . . . . . . . . 9
⊢ (𝑗 = 𝑖 → (𝑗 ∩ 𝑃) = (𝑖 ∩ 𝑃)) | 
| 58 | 57 | neeq1d 2999 | . . . . . . . 8
⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑃) ≠ ∅ ↔ (𝑖 ∩ 𝑃) ≠ ∅)) | 
| 59 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) | 
| 60 |  | 1arithufd.0 | . . . . . . . . . . 11
⊢  0 =
(0g‘𝑅) | 
| 61 | 59, 7, 60 | isufd 33569 | . . . . . . . . . 10
⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧
∀𝑗 ∈
((PrmIdeal‘𝑅) ∖
{{ 0
}})(𝑗 ∩ 𝑃) ≠
∅)) | 
| 62 | 61 | simprbi 496 | . . . . . . . . 9
⊢ (𝑅 ∈ UFD → ∀𝑗 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})(𝑗 ∩ 𝑃) ≠ ∅) | 
| 63 | 62 | adantr 480 | . . . . . . . 8
⊢ ((𝑅 ∈ UFD ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → ∀𝑗 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})(𝑗 ∩ 𝑃) ≠ ∅) | 
| 64 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑅 ∈ UFD ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) | 
| 65 | 58, 63, 64 | rspcdva 3622 | . . . . . . 7
⊢ ((𝑅 ∈ UFD ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → (𝑖 ∩ 𝑃) ≠ ∅) | 
| 66 | 39, 56, 65 | syl2anc 584 | . . . . . 6
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → (𝑖 ∩ 𝑃) ≠ ∅) | 
| 67 |  | sseq0 4402 | . . . . . . . . 9
⊢ (((𝑖 ∩ 𝑃) ⊆ (𝑖 ∩ 𝑆) ∧ (𝑖 ∩ 𝑆) = ∅) → (𝑖 ∩ 𝑃) = ∅) | 
| 68 | 67 | expcom 413 | . . . . . . . 8
⊢ ((𝑖 ∩ 𝑆) = ∅ → ((𝑖 ∩ 𝑃) ⊆ (𝑖 ∩ 𝑆) → (𝑖 ∩ 𝑃) = ∅)) | 
| 69 | 68 | necon3ad 2952 | . . . . . . 7
⊢ ((𝑖 ∩ 𝑆) = ∅ → ((𝑖 ∩ 𝑃) ≠ ∅ → ¬ (𝑖 ∩ 𝑃) ⊆ (𝑖 ∩ 𝑆))) | 
| 70 |  | sslin 4242 | . . . . . . . 8
⊢ (𝑃 ⊆ 𝑆 → (𝑖 ∩ 𝑃) ⊆ (𝑖 ∩ 𝑆)) | 
| 71 | 70 | con3i 154 | . . . . . . 7
⊢ (¬
(𝑖 ∩ 𝑃) ⊆ (𝑖 ∩ 𝑆) → ¬ 𝑃 ⊆ 𝑆) | 
| 72 | 69, 71 | syl6 35 | . . . . . 6
⊢ ((𝑖 ∩ 𝑆) = ∅ → ((𝑖 ∩ 𝑃) ≠ ∅ → ¬ 𝑃 ⊆ 𝑆)) | 
| 73 | 38, 66, 72 | sylc 65 | . . . . 5
⊢
((((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑆 ∩ 𝑖) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑖)) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → ¬ 𝑃 ⊆ 𝑆) | 
| 74 | 34, 73 | sylanbr 582 | . . . 4
⊢
(((((𝜑 ∧ ¬
𝑋 ∈ 𝑆) ∧ 𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)}) ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗) → ¬ 𝑃 ⊆ 𝑆) | 
| 75 | 74 | anasss 466 | . . 3
⊢ ((((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)}) ∧ (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗)) → ¬ 𝑃 ⊆ 𝑆) | 
| 76 | 42 | idomcringd 20728 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 77 | 76 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → 𝑅 ∈ CRing) | 
| 78 | 43 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → 𝑅 ∈ Ring) | 
| 79 | 44 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝐵) | 
| 80 | 79 | snssd 4808 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → {𝑋} ⊆ 𝐵) | 
| 81 |  | eqid 2736 | . . . . . 6
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 82 | 45, 6, 81 | rspcl 21246 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ {𝑋} ⊆ 𝐵) → ((RSpan‘𝑅)‘{𝑋}) ∈ (LIdeal‘𝑅)) | 
| 83 | 78, 80, 82 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → ((RSpan‘𝑅)‘{𝑋}) ∈ (LIdeal‘𝑅)) | 
| 84 | 15 | ringmgp 20237 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) | 
| 85 | 43, 84 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ Mnd) | 
| 86 | 21 | ssrab3 4081 | . . . . . . 7
⊢ 𝑆 ⊆ 𝐵 | 
| 87 | 86 | a1i 11 | . . . . . 6
⊢ (𝜑 → 𝑆 ⊆ 𝐵) | 
| 88 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑥 = (1r‘𝑅) → (𝑥 = (𝑀 Σg 𝑓) ↔
(1r‘𝑅) =
(𝑀
Σg 𝑓))) | 
| 89 | 88 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑥 = (1r‘𝑅) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(1r‘𝑅) = (𝑀 Σg 𝑓))) | 
| 90 |  | eqcom 2743 | . . . . . . . . . 10
⊢
((1r‘𝑅) = (𝑀 Σg 𝑓) ↔ (𝑀 Σg 𝑓) = (1r‘𝑅)) | 
| 91 | 90 | rexbii 3093 | . . . . . . . . 9
⊢
(∃𝑓 ∈
Word 𝑃(1r‘𝑅) = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑀 Σg 𝑓) = (1r‘𝑅)) | 
| 92 | 89, 91 | bitrdi 287 | . . . . . . . 8
⊢ (𝑥 = (1r‘𝑅) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃(𝑀 Σg 𝑓) = (1r‘𝑅))) | 
| 93 |  | eqid 2736 | . . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 94 | 6, 93 | ringidcl 20263 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) | 
| 95 | 43, 94 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) | 
| 96 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑓 = ∅ → (𝑀 Σg
𝑓) = (𝑀 Σg
∅)) | 
| 97 | 96 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑓 = ∅ → ((𝑀 Σg
𝑓) =
(1r‘𝑅)
↔ (𝑀
Σg ∅) = (1r‘𝑅))) | 
| 98 |  | wrd0 14578 | . . . . . . . . . 10
⊢ ∅
∈ Word 𝑃 | 
| 99 | 98 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ∅ ∈ Word 𝑃) | 
| 100 | 15, 93 | ringidval 20181 | . . . . . . . . . . 11
⊢
(1r‘𝑅) = (0g‘𝑀) | 
| 101 | 100 | gsum0 18698 | . . . . . . . . . 10
⊢ (𝑀 Σg
∅) = (1r‘𝑅) | 
| 102 | 101 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (𝑀 Σg ∅) =
(1r‘𝑅)) | 
| 103 | 97, 99, 102 | rspcedvdw 3624 | . . . . . . . 8
⊢ (𝜑 → ∃𝑓 ∈ Word 𝑃(𝑀 Σg 𝑓) = (1r‘𝑅)) | 
| 104 | 92, 95, 103 | elrabd 3693 | . . . . . . 7
⊢ (𝜑 → (1r‘𝑅) ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)}) | 
| 105 | 104, 21 | eleqtrrdi 2851 | . . . . . 6
⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆) | 
| 106 |  | 1arithufd.u | . . . . . . . . 9
⊢ 𝑈 = (Unit‘𝑅) | 
| 107 | 8 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → 𝑅 ∈ UFD) | 
| 108 |  | 1arithufdlem.2 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑅 ∈ DivRing) | 
| 109 | 108 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → ¬ 𝑅 ∈ DivRing) | 
| 110 |  | eqid 2736 | . . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 111 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → 𝑎 ∈ 𝑆) | 
| 112 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → 𝑏 ∈ 𝑆) | 
| 113 | 6, 60, 106, 7, 15, 107, 109, 21, 110, 111, 112 | 1arithufdlem2 33574 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑏 ∈ 𝑆) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑆) | 
| 114 | 113 | anasss 466 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎(.r‘𝑅)𝑏) ∈ 𝑆) | 
| 115 | 114 | ralrimivva 3201 | . . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 ∀𝑏 ∈ 𝑆 (𝑎(.r‘𝑅)𝑏) ∈ 𝑆) | 
| 116 | 15, 110 | mgpplusg 20142 | . . . . . . . 8
⊢
(.r‘𝑅) = (+g‘𝑀) | 
| 117 | 16, 100, 116 | issubm 18817 | . . . . . . 7
⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑎 ∈ 𝑆 ∀𝑏 ∈ 𝑆 (𝑎(.r‘𝑅)𝑏) ∈ 𝑆))) | 
| 118 | 117 | biimpar 477 | . . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ (𝑆 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑎 ∈ 𝑆 ∀𝑏 ∈ 𝑆 (𝑎(.r‘𝑅)𝑏) ∈ 𝑆)) → 𝑆 ∈ (SubMnd‘𝑀)) | 
| 119 | 85, 87, 105, 115, 118 | syl13anc 1373 | . . . . 5
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀)) | 
| 120 | 119 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → 𝑆 ∈ (SubMnd‘𝑀)) | 
| 121 |  | neq0 4351 | . . . . . . . . 9
⊢ (¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅ ↔ ∃𝑢 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) | 
| 122 | 121 | biimpi 216 | . . . . . . . 8
⊢ (¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅ → ∃𝑢 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) | 
| 123 | 122 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) → ∃𝑢 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) | 
| 124 | 8 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑅 ∈ UFD) | 
| 125 | 108 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → ¬ 𝑅 ∈ DivRing) | 
| 126 | 44 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑋 ∈ 𝐵) | 
| 127 |  | 1arithufdlem.4 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) | 
| 128 | 127 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → ¬ 𝑋 ∈ 𝑈) | 
| 129 | 50 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑋 ≠ 0 ) | 
| 130 |  | simplr 768 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑦 ∈ 𝐵) | 
| 131 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑢 = (𝑦(.r‘𝑅)𝑋)) | 
| 132 |  | simpllr 775 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) | 
| 133 | 132 | elin1d 4203 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑢 ∈ 𝑆) | 
| 134 | 131, 133 | eqeltrrd 2841 | . . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → (𝑦(.r‘𝑅)𝑋) ∈ 𝑆) | 
| 135 | 6, 60, 106, 7, 15, 124, 125, 21, 126, 128, 129, 110, 130, 134 | 1arithufdlem3 33575 | . . . . . . . 8
⊢
(((((𝜑 ∧ ¬
(𝑆 ∩
((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) ∧ 𝑦 ∈ 𝐵) ∧ 𝑢 = (𝑦(.r‘𝑅)𝑋)) → 𝑋 ∈ 𝑆) | 
| 136 | 43 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) → 𝑅 ∈ Ring) | 
| 137 | 44 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) → 𝑋 ∈ 𝐵) | 
| 138 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) → 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) | 
| 139 | 138 | elin2d 4204 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) → 𝑢 ∈ ((RSpan‘𝑅)‘{𝑋})) | 
| 140 | 6, 110, 45 | elrspsn 21251 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑢 ∈ ((RSpan‘𝑅)‘{𝑋}) ↔ ∃𝑦 ∈ 𝐵 𝑢 = (𝑦(.r‘𝑅)𝑋))) | 
| 141 | 140 | biimpa 476 | . . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) ∧ 𝑢 ∈ ((RSpan‘𝑅)‘{𝑋})) → ∃𝑦 ∈ 𝐵 𝑢 = (𝑦(.r‘𝑅)𝑋)) | 
| 142 | 136, 137,
139, 141 | syl21anc 837 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) → ∃𝑦 ∈ 𝐵 𝑢 = (𝑦(.r‘𝑅)𝑋)) | 
| 143 | 135, 142 | r19.29a 3161 | . . . . . . 7
⊢ (((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) ∧ 𝑢 ∈ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋}))) → 𝑋 ∈ 𝑆) | 
| 144 | 123, 143 | exlimddv 1934 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) → 𝑋 ∈ 𝑆) | 
| 145 | 144 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) → 𝑋 ∈ 𝑆) | 
| 146 |  | simplr 768 | . . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) ∧ ¬ (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) → ¬ 𝑋 ∈ 𝑆) | 
| 147 | 145, 146 | condan 817 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → (𝑆 ∩ ((RSpan‘𝑅)‘{𝑋})) = ∅) | 
| 148 |  | eqid 2736 | . . . 4
⊢ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} | 
| 149 | 6, 77, 83, 120, 15, 147, 148 | ssdifidlprm 33487 | . . 3
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → ∃𝑖 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ ((RSpan‘𝑅)‘{𝑋}) ⊆ 𝑝)} ¬ 𝑖 ⊊ 𝑗)) | 
| 150 | 75, 149 | r19.29a 3161 | . 2
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑆) → ¬ 𝑃 ⊆ 𝑆) | 
| 151 | 25, 150 | condan 817 | 1
⊢ (𝜑 → 𝑋 ∈ 𝑆) |