| Step | Hyp | Ref
| Expression |
| 1 | | rprmdvdsprod.3 |
. . 3
⊢ (𝜑 → 𝑄 ∥ (𝑀 Σg 𝐹)) |
| 2 | | rprmdvdsprod.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑅) |
| 3 | | rprmdvdsprod.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 4 | 2, 3 | mgpbas 20142 |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
| 5 | | rprmdvdsprod.1 |
. . . . . 6
⊢ 1 =
(1r‘𝑅) |
| 6 | 2, 5 | ringidval 20180 |
. . . . 5
⊢ 1 =
(0g‘𝑀) |
| 7 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 8 | 2, 7 | mgpplusg 20141 |
. . . . 5
⊢
(.r‘𝑅) = (+g‘𝑀) |
| 9 | | rprmdvdsprod.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 10 | 2 | crngmgp 20238 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑀 ∈ CMnd) |
| 11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ CMnd) |
| 12 | | rprmdvdsprod.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 13 | | rprmdvdsprod.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) |
| 14 | | rprmdvdsprod.2 |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp 1 ) |
| 15 | | disjdifr 4473 |
. . . . . 6
⊢ ((𝐼 ∖ (𝐹 supp 1 )) ∩ (𝐹 supp 1 )) =
∅ |
| 16 | 15 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝐼 ∖ (𝐹 supp 1 )) ∩ (𝐹 supp 1 )) =
∅) |
| 17 | | suppssdm 8202 |
. . . . . . . 8
⊢ (𝐹 supp 1 ) ⊆ dom 𝐹 |
| 18 | 17, 13 | fssdm 6755 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 1 ) ⊆ 𝐼) |
| 19 | | undifr 4483 |
. . . . . . 7
⊢ ((𝐹 supp 1 ) ⊆ 𝐼 ↔ ((𝐼 ∖ (𝐹 supp 1 )) ∪ (𝐹 supp 1 )) = 𝐼) |
| 20 | 18, 19 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ((𝐼 ∖ (𝐹 supp 1 )) ∪ (𝐹 supp 1 )) = 𝐼) |
| 21 | 20 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → 𝐼 = ((𝐼 ∖ (𝐹 supp 1 )) ∪ (𝐹 supp 1 ))) |
| 22 | 4, 6, 8, 11, 12, 13, 14, 16, 21 | gsumsplit 19946 |
. . . 4
⊢ (𝜑 → (𝑀 Σg 𝐹) = ((𝑀 Σg (𝐹 ↾ (𝐼 ∖ (𝐹 supp 1
))))(.r‘𝑅)(𝑀 Σg (𝐹 ↾ (𝐹 supp 1 ))))) |
| 23 | | difssd 4137 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 ∖ (𝐹 supp 1 )) ⊆ 𝐼) |
| 24 | 13, 23 | feqresmpt 6978 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ (𝐼 ∖ (𝐹 supp 1 ))) = (𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ (𝐹‘𝑧))) |
| 25 | 13 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn 𝐼) |
| 26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 ))) → 𝐹 Fn 𝐼) |
| 27 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 ))) → 𝐼 ∈ 𝑉) |
| 28 | 9 | crngringd 20243 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 29 | 3, 5 | ringidcl 20262 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ 𝐵) |
| 31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 ))) → 1 ∈ 𝐵) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 ))) → 𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 ))) |
| 33 | 26, 27, 31, 32 | fvdifsupp 8196 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 ))) → (𝐹‘𝑧) = 1 ) |
| 34 | 33 | mpteq2dva 5242 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ (𝐹‘𝑧)) = (𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ 1
)) |
| 35 | 24, 34 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ (𝐼 ∖ (𝐹 supp 1 ))) = (𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ 1
)) |
| 36 | 35 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ (𝐼 ∖ (𝐹 supp 1 )))) = (𝑀 Σg (𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ 1
))) |
| 37 | 11 | cmnmndd 19822 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ Mnd) |
| 38 | 12 | difexd 5331 |
. . . . . . 7
⊢ (𝜑 → (𝐼 ∖ (𝐹 supp 1 )) ∈
V) |
| 39 | 6 | gsumz 18849 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ (𝐼 ∖ (𝐹 supp 1 )) ∈ V) → (𝑀 Σg
(𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ 1 )) = 1
) |
| 40 | 37, 38, 39 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑀 Σg (𝑧 ∈ (𝐼 ∖ (𝐹 supp 1 )) ↦ 1 )) = 1
) |
| 41 | 36, 40 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ (𝐼 ∖ (𝐹 supp 1 )))) = 1 ) |
| 42 | 41 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((𝑀 Σg (𝐹 ↾ (𝐼 ∖ (𝐹 supp 1
))))(.r‘𝑅)(𝑀 Σg (𝐹 ↾ (𝐹 supp 1 )))) = ( 1
(.r‘𝑅)(𝑀 Σg (𝐹 ↾ (𝐹 supp 1 ))))) |
| 43 | | ovexd 7466 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 1 ) ∈
V) |
| 44 | 13, 18 | fssresd 6775 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 1 )):(𝐹 supp 1 )⟶𝐵) |
| 45 | 14, 30 | fsuppres 9433 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 1 )) finSupp 1
) |
| 46 | 4, 6, 11, 43, 44, 45 | gsumcl 19933 |
. . . . 5
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 ))) ∈ 𝐵) |
| 47 | 3, 7, 5, 28, 46 | ringlidmd 20269 |
. . . 4
⊢ (𝜑 → ( 1 (.r‘𝑅)(𝑀 Σg (𝐹 ↾ (𝐹 supp 1 )))) = (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 )))) |
| 48 | 22, 42, 47 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 )))) |
| 49 | 1, 48 | breqtrd 5169 |
. 2
⊢ (𝜑 → 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 )))) |
| 50 | | reseq2 5992 |
. . . . . 6
⊢ (𝑏 = ∅ → (𝐹 ↾ 𝑏) = (𝐹 ↾ ∅)) |
| 51 | 50 | oveq2d 7447 |
. . . . 5
⊢ (𝑏 = ∅ → (𝑀 Σg
(𝐹 ↾ 𝑏)) = (𝑀 Σg (𝐹 ↾
∅))) |
| 52 | 51 | breq2d 5155 |
. . . 4
⊢ (𝑏 = ∅ → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) ↔ 𝑄 ∥ (𝑀 Σg (𝐹 ↾
∅)))) |
| 53 | | rexeq 3322 |
. . . 4
⊢ (𝑏 = ∅ → (∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥) ↔ ∃𝑥 ∈ ∅ 𝑄 ∥ (𝐹‘𝑥))) |
| 54 | 52, 53 | imbi12d 344 |
. . 3
⊢ (𝑏 = ∅ → ((𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) → ∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥)) ↔ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ ∅)) →
∃𝑥 ∈ ∅
𝑄 ∥ (𝐹‘𝑥)))) |
| 55 | | reseq2 5992 |
. . . . . 6
⊢ (𝑏 = 𝑎 → (𝐹 ↾ 𝑏) = (𝐹 ↾ 𝑎)) |
| 56 | 55 | oveq2d 7447 |
. . . . 5
⊢ (𝑏 = 𝑎 → (𝑀 Σg (𝐹 ↾ 𝑏)) = (𝑀 Σg (𝐹 ↾ 𝑎))) |
| 57 | 56 | breq2d 5155 |
. . . 4
⊢ (𝑏 = 𝑎 → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) ↔ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)))) |
| 58 | | rexeq 3322 |
. . . 4
⊢ (𝑏 = 𝑎 → (∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) |
| 59 | 57, 58 | imbi12d 344 |
. . 3
⊢ (𝑏 = 𝑎 → ((𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) → ∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥)) ↔ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥)))) |
| 60 | | reseq2 5992 |
. . . . . 6
⊢ (𝑏 = (𝑎 ∪ {𝑦}) → (𝐹 ↾ 𝑏) = (𝐹 ↾ (𝑎 ∪ {𝑦}))) |
| 61 | 60 | oveq2d 7447 |
. . . . 5
⊢ (𝑏 = (𝑎 ∪ {𝑦}) → (𝑀 Σg (𝐹 ↾ 𝑏)) = (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) |
| 62 | 61 | breq2d 5155 |
. . . 4
⊢ (𝑏 = (𝑎 ∪ {𝑦}) → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) ↔ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦}))))) |
| 63 | | rexeq 3322 |
. . . 4
⊢ (𝑏 = (𝑎 ∪ {𝑦}) → (∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥) ↔ ∃𝑥 ∈ (𝑎 ∪ {𝑦})𝑄 ∥ (𝐹‘𝑥))) |
| 64 | 62, 63 | imbi12d 344 |
. . 3
⊢ (𝑏 = (𝑎 ∪ {𝑦}) → ((𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) → ∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥)) ↔ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦}))) → ∃𝑥 ∈ (𝑎 ∪ {𝑦})𝑄 ∥ (𝐹‘𝑥)))) |
| 65 | | reseq2 5992 |
. . . . . 6
⊢ (𝑏 = (𝐹 supp 1 ) → (𝐹 ↾ 𝑏) = (𝐹 ↾ (𝐹 supp 1 ))) |
| 66 | 65 | oveq2d 7447 |
. . . . 5
⊢ (𝑏 = (𝐹 supp 1 ) → (𝑀 Σg
(𝐹 ↾ 𝑏)) = (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 )))) |
| 67 | 66 | breq2d 5155 |
. . . 4
⊢ (𝑏 = (𝐹 supp 1 ) → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) ↔ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 ))))) |
| 68 | | rexeq 3322 |
. . . 4
⊢ (𝑏 = (𝐹 supp 1 ) → (∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥) ↔ ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥))) |
| 69 | 67, 68 | imbi12d 344 |
. . 3
⊢ (𝑏 = (𝐹 supp 1 ) → ((𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑏)) → ∃𝑥 ∈ 𝑏 𝑄 ∥ (𝐹‘𝑥)) ↔ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 ))) → ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥)))) |
| 70 | | rprmdvdsprod.d |
. . . . . 6
⊢ ∥ =
(∥r‘𝑅) |
| 71 | | rprmdvdsprod.p |
. . . . . 6
⊢ 𝑃 = (RPrime‘𝑅) |
| 72 | | rprmdvdsprod.q |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ 𝑃) |
| 73 | 5, 70, 71, 9, 72 | rprmndvdsr1 33552 |
. . . . 5
⊢ (𝜑 → ¬ 𝑄 ∥ 1 ) |
| 74 | | res0 6001 |
. . . . . . . . 9
⊢ (𝐹 ↾ ∅) =
∅ |
| 75 | 74 | oveq2i 7442 |
. . . . . . . 8
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
(𝑀
Σg ∅) |
| 76 | 6 | gsum0 18697 |
. . . . . . . 8
⊢ (𝑀 Σg
∅) = 1 |
| 77 | 75, 76 | eqtri 2765 |
. . . . . . 7
⊢ (𝑀 Σg
(𝐹 ↾ ∅)) =
1 |
| 78 | 77 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) = 1
) |
| 79 | 78 | breq2d 5155 |
. . . . 5
⊢ (𝜑 → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ ∅)) ↔ 𝑄 ∥ 1 )) |
| 80 | 73, 79 | mtbird 325 |
. . . 4
⊢ (𝜑 → ¬ 𝑄 ∥ (𝑀 Σg (𝐹 ↾
∅))) |
| 81 | 80 | pm2.21d 121 |
. . 3
⊢ (𝜑 → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ ∅)) →
∃𝑥 ∈ ∅
𝑄 ∥ (𝐹‘𝑥))) |
| 82 | | simpllr 776 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎))) → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) |
| 83 | 82 | syldbl2 842 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎))) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥)) |
| 84 | | simpr 484 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) ∧ 𝑄 ∥ (𝐹‘𝑦)) → 𝑄 ∥ (𝐹‘𝑦)) |
| 85 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 86 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 87 | 86 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑄 ∥ (𝐹‘𝑥) ↔ 𝑄 ∥ (𝐹‘𝑦))) |
| 88 | 85, 87 | rexsn 4682 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{𝑦}𝑄 ∥ (𝐹‘𝑥) ↔ 𝑄 ∥ (𝐹‘𝑦)) |
| 89 | 84, 88 | sylibr 234 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) ∧ 𝑄 ∥ (𝐹‘𝑦)) → ∃𝑥 ∈ {𝑦}𝑄 ∥ (𝐹‘𝑥)) |
| 90 | 9 | ad4antr 732 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑅 ∈ CRing) |
| 91 | 72 | ad4antr 732 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑄 ∈ 𝑃) |
| 92 | 90, 10 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑀 ∈ CMnd) |
| 93 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
| 94 | 93 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑎 ∈ V) |
| 95 | 13 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝐹:𝐼⟶𝐵) |
| 96 | | simp-4r 784 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑎 ⊆ (𝐹 supp 1 )) |
| 97 | 18 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹 supp 1 ) ⊆ 𝐼) |
| 98 | 96, 97 | sstrd 3994 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑎 ⊆ 𝐼) |
| 99 | 95, 98 | fssresd 6775 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹 ↾ 𝑎):𝑎⟶𝐵) |
| 100 | 14 | fsuppimpd 9409 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 1 ) ∈
Fin) |
| 101 | 100 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹 supp 1 ) ∈
Fin) |
| 102 | 101, 96 | ssfid 9301 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑎 ∈ Fin) |
| 103 | 30 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 1 ∈ 𝐵) |
| 104 | 99, 102, 103 | fdmfifsupp 9415 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹 ↾ 𝑎) finSupp 1 ) |
| 105 | 4, 6, 92, 94, 99, 104 | gsumcl 19933 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝑀 Σg (𝐹 ↾ 𝑎)) ∈ 𝐵) |
| 106 | 97 | ssdifssd 4147 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → ((𝐹 supp 1 ) ∖ 𝑎) ⊆ 𝐼) |
| 107 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) |
| 108 | 106, 107 | sseldd 3984 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑦 ∈ 𝐼) |
| 109 | 95, 108 | ffvelcdmd 7105 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹‘𝑦) ∈ 𝐵) |
| 110 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) |
| 111 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Cntz‘𝑀) =
(Cntz‘𝑀) |
| 112 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐹‘𝑦) = (𝐹‘𝑦) |
| 113 | 37 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑀 ∈ Mnd) |
| 114 | 107 | eldifbd 3964 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → ¬ 𝑦 ∈ 𝑎) |
| 115 | 95 | fimassd 6757 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹 “ (𝑎 ∪ {𝑦})) ⊆ 𝐵) |
| 116 | 4, 111 | cntzcmn 19858 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ CMnd ∧ (𝐹 “ (𝑎 ∪ {𝑦})) ⊆ 𝐵) → ((Cntz‘𝑀)‘(𝐹 “ (𝑎 ∪ {𝑦}))) = 𝐵) |
| 117 | 92, 115, 116 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → ((Cntz‘𝑀)‘(𝐹 “ (𝑎 ∪ {𝑦}))) = 𝐵) |
| 118 | 115, 117 | sseqtrrd 4021 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝐹 “ (𝑎 ∪ {𝑦})) ⊆ ((Cntz‘𝑀)‘(𝐹 “ (𝑎 ∪ {𝑦})))) |
| 119 | 4, 8, 111, 112, 95, 98, 113, 102, 114, 108, 109, 118 | gsumzresunsn 33059 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦}))) = ((𝑀 Σg (𝐹 ↾ 𝑎))(.r‘𝑅)(𝐹‘𝑦))) |
| 120 | 110, 119 | breqtrd 5169 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → 𝑄 ∥ ((𝑀 Σg (𝐹 ↾ 𝑎))(.r‘𝑅)(𝐹‘𝑦))) |
| 121 | 3, 71, 70, 7, 90, 91, 105, 109, 120 | rprmdvds 33547 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) ∨ 𝑄 ∥ (𝐹‘𝑦))) |
| 122 | 83, 89, 121 | orim12da 32477 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → (∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥) ∨ ∃𝑥 ∈ {𝑦}𝑄 ∥ (𝐹‘𝑥))) |
| 123 | | rexun 4196 |
. . . . . 6
⊢
(∃𝑥 ∈
(𝑎 ∪ {𝑦})𝑄 ∥ (𝐹‘𝑥) ↔ (∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥) ∨ ∃𝑥 ∈ {𝑦}𝑄 ∥ (𝐹‘𝑥))) |
| 124 | 122, 123 | sylibr 234 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) ∧ (𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥))) ∧ 𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦})))) → ∃𝑥 ∈ (𝑎 ∪ {𝑦})𝑄 ∥ (𝐹‘𝑥)) |
| 125 | 124 | exp31 419 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ⊆ (𝐹 supp 1 )) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎)) → ((𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥)) → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦}))) → ∃𝑥 ∈ (𝑎 ∪ {𝑦})𝑄 ∥ (𝐹‘𝑥)))) |
| 126 | 125 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ⊆ (𝐹 supp 1 ) ∧ 𝑦 ∈ ((𝐹 supp 1 ) ∖ 𝑎))) → ((𝑄 ∥ (𝑀 Σg (𝐹 ↾ 𝑎)) → ∃𝑥 ∈ 𝑎 𝑄 ∥ (𝐹‘𝑥)) → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝑎 ∪ {𝑦}))) → ∃𝑥 ∈ (𝑎 ∪ {𝑦})𝑄 ∥ (𝐹‘𝑥)))) |
| 127 | 54, 59, 64, 69, 81, 126, 100 | findcard2d 9206 |
. 2
⊢ (𝜑 → (𝑄 ∥ (𝑀 Σg (𝐹 ↾ (𝐹 supp 1 ))) → ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥))) |
| 128 | 49, 127 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ (𝐹 supp 1 )𝑄 ∥ (𝐹‘𝑥)) |