| Step | Hyp | Ref
| Expression |
| 1 | | mnringmulrcld.2 |
. . 3
⊢ 𝐹 = (𝑅 MndRing 𝑀) |
| 2 | | mnringmulrcld.3 |
. . 3
⊢ 𝐵 = (Base‘𝐹) |
| 3 | | eqid 2737 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 4 | | eqid 2737 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 5 | | mnringmulrcld.1 |
. . 3
⊢ 𝐴 = (Base‘𝑀) |
| 6 | | eqid 2737 |
. . 3
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 7 | | mnringmulrcld.4 |
. . 3
⊢ · =
(.r‘𝐹) |
| 8 | | mnringmulrcld.5 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 9 | | mnringmulrcld.6 |
. . 3
⊢ (𝜑 → 𝑀 ∈ 𝑈) |
| 10 | | mnringmulrcld.7 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 11 | | mnringmulrcld.8 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | mnringmulrvald 44246 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))))) |
| 13 | | eqid 2737 |
. . 3
⊢
(0g‘𝐹) = (0g‘𝐹) |
| 14 | 1, 8, 9 | mnringlmodd 44245 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ LMod) |
| 15 | | lmodcmn 20908 |
. . . 4
⊢ (𝐹 ∈ LMod → 𝐹 ∈ CMnd) |
| 16 | 14, 15 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 ∈ CMnd) |
| 17 | 5 | fvexi 6920 |
. . . . 5
⊢ 𝐴 ∈ V |
| 18 | 17, 17 | xpex 7773 |
. . . 4
⊢ (𝐴 × 𝐴) ∈ V |
| 19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 × 𝐴) ∈ V) |
| 20 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑅 ∈ Ring) |
| 21 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 22 | 1, 2, 5, 21, 8, 9,
10 | mnringbasefd 44234 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋:𝐴⟶(Base‘𝑅)) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑋:𝐴⟶(Base‘𝑅)) |
| 24 | | simp2 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
| 25 | 23, 24 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑋‘𝑎) ∈ (Base‘𝑅)) |
| 26 | 1, 2, 5, 21, 8, 9,
11 | mnringbasefd 44234 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌:𝐴⟶(Base‘𝑅)) |
| 27 | 26 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑌:𝐴⟶(Base‘𝑅)) |
| 28 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) |
| 29 | 27, 28 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑌‘𝑏) ∈ (Base‘𝑅)) |
| 30 | 21, 3 | ringcl 20247 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑎) ∈ (Base‘𝑅) ∧ (𝑌‘𝑏) ∈ (Base‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) ∈ (Base‘𝑅)) |
| 31 | 20, 25, 29, 30 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) ∈ (Base‘𝑅)) |
| 32 | 21, 4 | ring0cl 20264 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
| 33 | 20, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (0g‘𝑅) ∈ (Base‘𝑅)) |
| 34 | 31, 33 | ifcld 4572 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) ∈ (Base‘𝑅)) |
| 35 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑖 ∈ 𝐴) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) ∈ (Base‘𝑅)) |
| 36 | 35 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))):𝐴⟶(Base‘𝑅)) |
| 37 | 21 | fvexi 6920 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
| 38 | 37, 17 | elmap 8911 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ↔ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))):𝐴⟶(Base‘𝑅)) |
| 39 | 36, 38 | sylibr 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴)) |
| 40 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝐴 ∈ V) |
| 41 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) |
| 42 | 40, 33, 41 | sniffsupp 9440 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅)) |
| 43 | 39, 42 | jca 511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ∧ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅))) |
| 44 | 9 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ 𝑈) |
| 45 | 1, 2, 5, 21, 4, 20, 44 | mnringelbased 44233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵 ↔ ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ∧ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅)))) |
| 46 | 43, 45 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵) |
| 47 | 46 | 3expb 1121 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵) |
| 48 | 47 | ralrimivva 3202 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵) |
| 49 | | eqid 2737 |
. . . . 5
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
| 50 | 49 | fmpo 8093 |
. . . 4
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐴 (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵 ↔ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))):(𝐴 × 𝐴)⟶𝐵) |
| 51 | 48, 50 | sylib 218 |
. . 3
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))):(𝐴 × 𝐴)⟶𝐵) |
| 52 | 17, 17 | mpoex 8104 |
. . . . 5
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) ∈ V |
| 53 | 52 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) ∈ V) |
| 54 | 51 | ffnd 6737 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) Fn (𝐴 × 𝐴)) |
| 55 | 13 | fvexi 6920 |
. . . . 5
⊢
(0g‘𝐹) ∈ V |
| 56 | 55 | a1i 11 |
. . . 4
⊢ (𝜑 → (0g‘𝐹) ∈ V) |
| 57 | 1, 2, 4, 8, 9, 10 | mnringbasefsuppd 44235 |
. . . . . 6
⊢ (𝜑 → 𝑋 finSupp (0g‘𝑅)) |
| 58 | 57 | fsuppimpd 9409 |
. . . . 5
⊢ (𝜑 → (𝑋 supp (0g‘𝑅)) ∈ Fin) |
| 59 | 1, 2, 4, 8, 9, 11 | mnringbasefsuppd 44235 |
. . . . . 6
⊢ (𝜑 → 𝑌 finSupp (0g‘𝑅)) |
| 60 | 59 | fsuppimpd 9409 |
. . . . 5
⊢ (𝜑 → (𝑌 supp (0g‘𝑅)) ∈ Fin) |
| 61 | | xpfi 9358 |
. . . . 5
⊢ (((𝑋 supp (0g‘𝑅)) ∈ Fin ∧ (𝑌 supp (0g‘𝑅)) ∈ Fin) → ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∈ Fin) |
| 62 | 58, 60, 61 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∈ Fin) |
| 63 | | elxpi 5707 |
. . . . . . 7
⊢ (𝑝 ∈ (𝐴 × 𝐴) → ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) |
| 64 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑝 = 〈𝑎, 𝑏〉) |
| 65 | 64 | 2eximi 1836 |
. . . . . . 7
⊢
(∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉) |
| 66 | 63, 65 | syl 17 |
. . . . . 6
⊢ (𝑝 ∈ (𝐴 × 𝐴) → ∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉) |
| 67 | 66 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → ∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉) |
| 68 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑎(𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) |
| 69 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑎 𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) |
| 70 | | nfmpo1 7513 |
. . . . . . . . 9
⊢
Ⅎ𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
| 71 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑎𝑝 |
| 72 | 70, 71 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑎((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) |
| 73 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑎(0g‘𝐹) |
| 74 | 72, 73 | nfeq 2919 |
. . . . . . 7
⊢
Ⅎ𝑎((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) |
| 75 | 69, 74 | nfor 1904 |
. . . . . 6
⊢
Ⅎ𝑎(𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) |
| 76 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑏(𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) |
| 77 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑏 𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) |
| 78 | | nfmpo2 7514 |
. . . . . . . . . 10
⊢
Ⅎ𝑏(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
| 79 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑏𝑝 |
| 80 | 78, 79 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑏((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) |
| 81 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑏(0g‘𝐹) |
| 82 | 80, 81 | nfeq 2919 |
. . . . . . . 8
⊢
Ⅎ𝑏((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) |
| 83 | 77, 82 | nfor 1904 |
. . . . . . 7
⊢
Ⅎ𝑏(𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) |
| 84 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑝 = 〈𝑎, 𝑏〉) |
| 85 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑝 ∈ (𝐴 × 𝐴)) |
| 86 | 84, 85 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐴)) |
| 87 | | opelxp 5721 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐴) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) |
| 88 | 86, 87 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) |
| 89 | | ianor 984 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ↔ (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
| 90 | 22 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋 Fn 𝐴) |
| 91 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ V) |
| 92 | 4 | fvexi 6920 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0g‘𝑅) ∈ V |
| 93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
| 94 | | elsuppfn 8195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 Fn 𝐴 ∧ 𝐴 ∈ V ∧ (0g‘𝑅) ∈ V) → (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)))) |
| 95 | 90, 91, 93, 94 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)))) |
| 96 | 95 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)) → 𝑎 ∈ (𝑋 supp (0g‘𝑅)))) |
| 97 | 96 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)) → 𝑎 ∈ (𝑋 supp (0g‘𝑅)))) |
| 98 | 24, 97 | mpand 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎) ≠ (0g‘𝑅) → 𝑎 ∈ (𝑋 supp (0g‘𝑅)))) |
| 99 | 98 | necon1bd 2958 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) → (𝑋‘𝑎) = (0g‘𝑅))) |
| 100 | 26 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑌 Fn 𝐴) |
| 101 | | elsuppfn 8195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑌 Fn 𝐴 ∧ 𝐴 ∈ V ∧ (0g‘𝑅) ∈ V) → (𝑏 ∈ (𝑌 supp (0g‘𝑅)) ↔ (𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)))) |
| 102 | 100, 91, 93, 101 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑏 ∈ (𝑌 supp (0g‘𝑅)) ↔ (𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)))) |
| 103 | 102 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)) → 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
| 104 | 103 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)) → 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
| 105 | 28, 104 | mpand 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑌‘𝑏) ≠ (0g‘𝑅) → 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
| 106 | 105 | necon1bd 2958 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)) → (𝑌‘𝑏) = (0g‘𝑅))) |
| 107 | 99, 106 | orim12d 967 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅)))) |
| 108 | 107 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) |
| 109 | 89, 108 | sylan2b 594 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) |
| 110 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋‘𝑎) = (0g‘𝑅) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏))) |
| 111 | 21, 3, 4 | ringlz 20290 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑏) ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
| 112 | 20, 29, 111 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
| 113 | 110, 112 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (𝑋‘𝑎) = (0g‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
| 114 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌‘𝑏) = (0g‘𝑅) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅))) |
| 115 | 21, 3, 4 | ringrz 20291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑎) ∈ (Base‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 116 | 20, 25, 115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 117 | 114, 116 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (𝑌‘𝑏) = (0g‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
| 118 | 113, 117 | jaodan 960 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
| 119 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) ∧ 𝑖 = (𝑎(+g‘𝑀)𝑏)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
| 120 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) ∧ ¬ 𝑖 = (𝑎(+g‘𝑀)𝑏)) → (0g‘𝑅) = (0g‘𝑅)) |
| 121 | 119, 120 | ifeqda 4562 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) = (0g‘𝑅)) |
| 122 | 121 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (𝑖 ∈ 𝐴 ↦ (0g‘𝑅))) |
| 123 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ×
{(0g‘𝑅)})
= (𝑖 ∈ 𝐴 ↦
(0g‘𝑅)) |
| 124 | 1, 4, 5, 8, 9 | mnring0g2d 44239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝐹)) |
| 125 | 123, 124 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹)) |
| 126 | 125 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹)) |
| 127 | 126 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹)) |
| 128 | 122, 127 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)) |
| 129 | 109, 128 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)) |
| 130 | 129 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
| 131 | 130 | orrd 864 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
| 132 | 131 | 3expb 1121 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
| 133 | 132 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
| 134 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ 〈𝑎, 𝑏〉 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))))) |
| 135 | | opelxp 5721 |
. . . . . . . . . . . . 13
⊢
(〈𝑎, 𝑏〉 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
| 136 | 134, 135 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))))) |
| 137 | 136 | 3ad2ant3 1136 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))))) |
| 138 | | simp2l 1200 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑎 ∈ 𝐴) |
| 139 | | simp2r 1201 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑏 ∈ 𝐴) |
| 140 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))) |
| 141 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑝 = 〈𝑎, 𝑏〉) |
| 142 | 17 | mptex 7243 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ V |
| 143 | 142 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ V) |
| 144 | 140, 141,
143 | fvmpopr2d 7595 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
| 145 | 138, 139,
144 | mpd3an23 1465 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
| 146 | 145 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) ↔ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
| 147 | 137, 146 | orbi12d 919 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → ((𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) ↔ ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))) |
| 148 | 133, 147 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))) |
| 149 | 88, 148 | syld3an2 1413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))) |
| 150 | 149 | 3expia 1122 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))) |
| 151 | 76, 83, 150 | exlimd 2218 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (∃𝑏 𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))) |
| 152 | 68, 75, 151 | exlimd 2218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))) |
| 153 | 67, 152 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))) |
| 154 | 53, 54, 56, 62, 153 | finnzfsuppd 9413 |
. . 3
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) finSupp (0g‘𝐹)) |
| 155 | 2, 13, 16, 19, 51, 154 | gsumcl 19933 |
. 2
⊢ (𝜑 → (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))) ∈ 𝐵) |
| 156 | 12, 155 | eqeltrd 2841 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) |