Step | Hyp | Ref
| Expression |
1 | | mnringmulrcld.2 |
. . 3
⊢ 𝐹 = (𝑅 MndRing 𝑀) |
2 | | mnringmulrcld.3 |
. . 3
⊢ 𝐵 = (Base‘𝐹) |
3 | | eqid 2759 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | eqid 2759 |
. . 3
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | mnringmulrcld.1 |
. . 3
⊢ 𝐴 = (Base‘𝑀) |
6 | | eqid 2759 |
. . 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 41293 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))))) |
13 | | eqid 2759 |
. . 3
⊢
(0g‘𝐹) = (0g‘𝐹) |
14 | 1, 8, 9 | mnringlmodd 41292 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ LMod) |
15 | | lmodcmn 19735 |
. . . 4
⊢ (𝐹 ∈ LMod → 𝐹 ∈ CMnd) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 ∈ CMnd) |
17 | 5 | fvexi 6665 |
. . . . 5
⊢ 𝐴 ∈ V |
18 | 17, 17 | xpex 7467 |
. . . 4
⊢ (𝐴 × 𝐴) ∈ V |
19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 × 𝐴) ∈ V) |
20 | 8 | 3ad2ant1 1131 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑅 ∈ Ring) |
21 | | eqid 2759 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘𝑅) |
22 | 1, 2, 5, 21, 8, 9,
10 | mnringbasefd 41284 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋:𝐴⟶(Base‘𝑅)) |
23 | 22 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑋:𝐴⟶(Base‘𝑅)) |
24 | | simp2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
25 | 23, 24 | ffvelrnd 6836 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑋‘𝑎) ∈ (Base‘𝑅)) |
26 | 1, 2, 5, 21, 8, 9,
11 | mnringbasefd 41284 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌:𝐴⟶(Base‘𝑅)) |
27 | 26 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑌:𝐴⟶(Base‘𝑅)) |
28 | | simp3 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) |
29 | 27, 28 | ffvelrnd 6836 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑌‘𝑏) ∈ (Base‘𝑅)) |
30 | 21, 3 | ringcl 19367 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑎) ∈ (Base‘𝑅) ∧ (𝑌‘𝑏) ∈ (Base‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) ∈ (Base‘𝑅)) |
31 | 20, 25, 29, 30 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) ∈ (Base‘𝑅)) |
32 | 21, 4 | ring0cl 19375 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
33 | 20, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (0g‘𝑅) ∈ (Base‘𝑅)) |
34 | 31, 33 | ifcld 4459 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) ∈ (Base‘𝑅)) |
35 | 34 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑖 ∈ 𝐴) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) ∈ (Base‘𝑅)) |
36 | 35 | fmpttd 6863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))):𝐴⟶(Base‘𝑅)) |
37 | 21 | fvexi 6665 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
38 | 37, 17 | elmap 8446 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ↔ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))):𝐴⟶(Base‘𝑅)) |
39 | 36, 38 | sylibr 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴)) |
40 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝐴 ∈ V) |
41 | | eqid 2759 |
. . . . . . . . 9
⊢ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) |
42 | 40, 33, 41 | sniffsupp 8882 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅)) |
43 | 39, 42 | jca 516 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ∧ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅))) |
44 | 9 | 3ad2ant1 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ 𝑈) |
45 | 1, 2, 5, 21, 4, 20, 44 | mnringelbased 41283 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵 ↔ ((𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ ((Base‘𝑅) ↑m 𝐴) ∧ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) finSupp (0g‘𝑅)))) |
46 | 43, 45 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵) |
47 | 46 | 3expb 1118 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵) |
48 | 47 | ralrimivva 3118 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵) |
49 | | eqid 2759 |
. . . . 5
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
50 | 49 | fmpo 7763 |
. . . 4
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐴 (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ 𝐵 ↔ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))):(𝐴 × 𝐴)⟶𝐵) |
51 | 48, 50 | sylib 221 |
. . 3
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))):(𝐴 × 𝐴)⟶𝐵) |
52 | 17, 17 | mpoex 7775 |
. . . . 5
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) ∈ V |
53 | 52 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) ∈ V) |
54 | 51 | ffnd 6492 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) Fn (𝐴 × 𝐴)) |
55 | 13 | fvexi 6665 |
. . . . 5
⊢
(0g‘𝐹) ∈ V |
56 | 55 | a1i 11 |
. . . 4
⊢ (𝜑 → (0g‘𝐹) ∈ V) |
57 | 1, 2, 4, 8, 9, 10 | mnringbasefsuppd 41285 |
. . . . . 6
⊢ (𝜑 → 𝑋 finSupp (0g‘𝑅)) |
58 | 57 | fsuppimpd 8858 |
. . . . 5
⊢ (𝜑 → (𝑋 supp (0g‘𝑅)) ∈ Fin) |
59 | 1, 2, 4, 8, 9, 11 | mnringbasefsuppd 41285 |
. . . . . 6
⊢ (𝜑 → 𝑌 finSupp (0g‘𝑅)) |
60 | 59 | fsuppimpd 8858 |
. . . . 5
⊢ (𝜑 → (𝑌 supp (0g‘𝑅)) ∈ Fin) |
61 | | xpfi 8807 |
. . . . 5
⊢ (((𝑋 supp (0g‘𝑅)) ∈ Fin ∧ (𝑌 supp (0g‘𝑅)) ∈ Fin) → ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∈ Fin) |
62 | 58, 60, 61 | syl2anc 588 |
. . . 4
⊢ (𝜑 → ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∈ Fin) |
63 | | elxpi 5539 |
. . . . . . 7
⊢ (𝑝 ∈ (𝐴 × 𝐴) → ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) |
64 | | simpl 487 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑝 = 〈𝑎, 𝑏〉) |
65 | 64 | 2eximi 1838 |
. . . . . . 7
⊢
(∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉) |
66 | 63, 65 | syl 17 |
. . . . . 6
⊢ (𝑝 ∈ (𝐴 × 𝐴) → ∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉) |
67 | 66 | adantl 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → ∃𝑎∃𝑏 𝑝 = 〈𝑎, 𝑏〉) |
68 | | nfv 1916 |
. . . . . 6
⊢
Ⅎ𝑎(𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) |
69 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑎 𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) |
70 | | nfmpo1 7221 |
. . . . . . . . 9
⊢
Ⅎ𝑎(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
71 | | nfcv 2917 |
. . . . . . . . 9
⊢
Ⅎ𝑎𝑝 |
72 | 70, 71 | nffv 6661 |
. . . . . . . 8
⊢
Ⅎ𝑎((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) |
73 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑎(0g‘𝐹) |
74 | 72, 73 | nfeq 2930 |
. . . . . . 7
⊢
Ⅎ𝑎((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) |
75 | 69, 74 | nfor 1906 |
. . . . . 6
⊢
Ⅎ𝑎(𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) |
76 | | nfv 1916 |
. . . . . . 7
⊢
Ⅎ𝑏(𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) |
77 | | nfv 1916 |
. . . . . . . 8
⊢
Ⅎ𝑏 𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) |
78 | | nfmpo2 7222 |
. . . . . . . . . 10
⊢
Ⅎ𝑏(𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
79 | | nfcv 2917 |
. . . . . . . . . 10
⊢
Ⅎ𝑏𝑝 |
80 | 78, 79 | nffv 6661 |
. . . . . . . . 9
⊢
Ⅎ𝑏((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) |
81 | | nfcv 2917 |
. . . . . . . . 9
⊢
Ⅎ𝑏(0g‘𝐹) |
82 | 80, 81 | nfeq 2930 |
. . . . . . . 8
⊢
Ⅎ𝑏((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) |
83 | 77, 82 | nfor 1906 |
. . . . . . 7
⊢
Ⅎ𝑏(𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) |
84 | | simp3 1136 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑝 = 〈𝑎, 𝑏〉) |
85 | | simp2 1135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑝 ∈ (𝐴 × 𝐴)) |
86 | 84, 85 | eqeltrrd 2852 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐴)) |
87 | | opelxp 5553 |
. . . . . . . . . 10
⊢
(〈𝑎, 𝑏〉 ∈ (𝐴 × 𝐴) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) |
88 | 86, 87 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) |
89 | | ianor 980 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ↔ (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
90 | 22 | ffnd 6492 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋 Fn 𝐴) |
91 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ V) |
92 | 4 | fvexi 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0g‘𝑅) ∈ V |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
94 | | elsuppfn 7838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 Fn 𝐴 ∧ 𝐴 ∈ V ∧ (0g‘𝑅) ∈ V) → (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)))) |
95 | 90, 91, 93, 94 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ↔ (𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)))) |
96 | 95 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)) → 𝑎 ∈ (𝑋 supp (0g‘𝑅)))) |
97 | 96 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ 𝐴 ∧ (𝑋‘𝑎) ≠ (0g‘𝑅)) → 𝑎 ∈ (𝑋 supp (0g‘𝑅)))) |
98 | 24, 97 | mpand 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎) ≠ (0g‘𝑅) → 𝑎 ∈ (𝑋 supp (0g‘𝑅)))) |
99 | 98 | necon1bd 2967 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) → (𝑋‘𝑎) = (0g‘𝑅))) |
100 | 26 | ffnd 6492 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑌 Fn 𝐴) |
101 | | elsuppfn 7838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑌 Fn 𝐴 ∧ 𝐴 ∈ V ∧ (0g‘𝑅) ∈ V) → (𝑏 ∈ (𝑌 supp (0g‘𝑅)) ↔ (𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)))) |
102 | 100, 91, 93, 101 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑏 ∈ (𝑌 supp (0g‘𝑅)) ↔ (𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)))) |
103 | 102 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)) → 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
104 | 103 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑏 ∈ 𝐴 ∧ (𝑌‘𝑏) ≠ (0g‘𝑅)) → 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
105 | 28, 104 | mpand 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑌‘𝑏) ≠ (0g‘𝑅) → 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
106 | 105 | necon1bd 2967 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)) → (𝑌‘𝑏) = (0g‘𝑅))) |
107 | 99, 106 | orim12d 963 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅)))) |
108 | 107 | imp 411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (¬ 𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∨ ¬ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) |
109 | 89, 108 | sylan2b 597 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) |
110 | | oveq1 7150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋‘𝑎) = (0g‘𝑅) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏))) |
111 | 21, 3, 4 | ringlz 19393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Ring ∧ (𝑌‘𝑏) ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
112 | 20, 29, 111 | syl2anc 588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((0g‘𝑅)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
113 | 110, 112 | sylan9eqr 2816 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (𝑋‘𝑎) = (0g‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
114 | | oveq2 7151 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌‘𝑏) = (0g‘𝑅) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅))) |
115 | 21, 3, 4 | ringrz 19394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑎) ∈ (Base‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
116 | 20, 25, 115 | syl2anc 588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑋‘𝑎)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
117 | 114, 116 | sylan9eqr 2816 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ (𝑌‘𝑏) = (0g‘𝑅)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
118 | 113, 117 | jaodan 956 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
119 | 118 | adantr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) ∧ 𝑖 = (𝑎(+g‘𝑀)𝑏)) → ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)) = (0g‘𝑅)) |
120 | | eqidd 2760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) ∧ ¬ 𝑖 = (𝑎(+g‘𝑀)𝑏)) → (0g‘𝑅) = (0g‘𝑅)) |
121 | 119, 120 | ifeqda 4449 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)) = (0g‘𝑅)) |
122 | 121 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (𝑖 ∈ 𝐴 ↦ (0g‘𝑅))) |
123 | | fconstmpt 5576 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ×
{(0g‘𝑅)})
= (𝑖 ∈ 𝐴 ↦
(0g‘𝑅)) |
124 | 1, 4, 5, 8, 9 | mnring0g2d 41288 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 × {(0g‘𝑅)}) = (0g‘𝐹)) |
125 | 123, 124 | syl5eqr 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹)) |
126 | 125 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹)) |
127 | 126 | adantr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ (0g‘𝑅)) = (0g‘𝐹)) |
128 | 122, 127 | eqtrd 2794 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ((𝑋‘𝑎) = (0g‘𝑅) ∨ (𝑌‘𝑏) = (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)) |
129 | 109, 128 | syldan 595 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)) |
130 | 129 | ex 417 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
131 | 130 | orrd 861 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
132 | 131 | 3expb 1118 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
133 | 132 | 3adant3 1130 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
134 | | eleq1 2838 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ 〈𝑎, 𝑏〉 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))))) |
135 | | opelxp 5553 |
. . . . . . . . . . . . 13
⊢
(〈𝑎, 𝑏〉 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅)))) |
136 | 134, 135 | syl6bb 291 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))))) |
137 | 136 | 3ad2ant3 1133 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ↔ (𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))))) |
138 | | simp2l 1197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑎 ∈ 𝐴) |
139 | | simp2r 1198 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑏 ∈ 𝐴) |
140 | | eqidd 2760 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))) |
141 | | simp3 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → 𝑝 = 〈𝑎, 𝑏〉) |
142 | 17 | mptex 6970 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ V |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) ∈ V) |
144 | 140, 141,
143 | fvmpopr2d 7299 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
145 | 138, 139,
144 | mpd3an23 1461 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) |
146 | 145 | eqeq1d 2761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹) ↔ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹))) |
147 | 137, 146 | orbi12d 917 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → ((𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)) ↔ ((𝑎 ∈ (𝑋 supp (0g‘𝑅)) ∧ 𝑏 ∈ (𝑌 supp (0g‘𝑅))) ∨ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))) = (0g‘𝐹)))) |
148 | 133, 147 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))) |
149 | 88, 148 | syld3an2 1409 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴) ∧ 𝑝 = 〈𝑎, 𝑏〉) → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹))) |
150 | 149 | 3expia 1119 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))) |
151 | 76, 83, 150 | exlimd 2217 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐴 × 𝐴)) → (∃𝑏 𝑝 = 〈𝑎, 𝑏〉 → (𝑝 ∈ ((𝑋 supp (0g‘𝑅)) × (𝑌 supp (0g‘𝑅))) ∨ ((𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))‘𝑝) = (0g‘𝐹)))) |
152 | 68, 75, 151 | exlimd 2217 |
. . . . 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 41273 |
. . 3
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅)))) finSupp (0g‘𝐹)) |
155 | 2, 13, 16, 19, 51, 154 | gsumcl 19088 |
. 2
⊢ (𝜑 → (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎(+g‘𝑀)𝑏), ((𝑋‘𝑎)(.r‘𝑅)(𝑌‘𝑏)), (0g‘𝑅))))) ∈ 𝐵) |
156 | 12, 155 | eqeltrd 2851 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) |