Step | Hyp | Ref
| Expression |
1 | | mamurid.f |
. . . . 5
⊢ 𝐹 = (𝑅 maMul 〈𝑁, 𝑀, 𝑀〉) |
2 | | mamumat1cl.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
3 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | mamumat1cl.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | 4 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑅 ∈ Ring) |
6 | | mamulid.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ Fin) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑁 ∈ Fin) |
8 | | mamumat1cl.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Fin) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑀 ∈ Fin) |
10 | | mamurid.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀))) |
11 | 10 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀))) |
12 | | mamumat1cl.o |
. . . . . . 7
⊢ 1 =
(1r‘𝑅) |
13 | | mamumat1cl.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑅) |
14 | | mamumat1cl.i |
. . . . . . 7
⊢ 𝐼 = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑀 ↦ if(𝑖 = 𝑗, 1 , 0 )) |
15 | 2, 4, 12, 13, 14, 8 | mamumat1cl 21336 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀))) |
16 | 15 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀))) |
17 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑙 ∈ 𝑁) |
18 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑚 ∈ 𝑀) |
19 | 1, 2, 3, 5, 7, 9, 9, 11, 16, 17, 18 | mamufv 21286 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙(𝑋𝐹𝐼)𝑚) = (𝑅 Σg (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))))) |
20 | | ringmnd 19572 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
21 | 5, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑅 ∈ Mnd) |
22 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑅 ∈ Ring) |
23 | | elmapi 8530 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀)) → 𝑋:(𝑁 × 𝑀)⟶𝐵) |
24 | 10, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:(𝑁 × 𝑀)⟶𝐵) |
25 | 24 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑋:(𝑁 × 𝑀)⟶𝐵) |
26 | | simplrl 777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑙 ∈ 𝑁) |
27 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑘 ∈ 𝑀) |
28 | 25, 26, 27 | fovrnd 7380 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → (𝑙𝑋𝑘) ∈ 𝐵) |
29 | | elmapi 8530 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀)) → 𝐼:(𝑀 × 𝑀)⟶𝐵) |
30 | 15, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼:(𝑀 × 𝑀)⟶𝐵) |
31 | 30 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝐼:(𝑀 × 𝑀)⟶𝐵) |
32 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑚 ∈ 𝑀) |
33 | 31, 27, 32 | fovrnd 7380 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → (𝑘𝐼𝑚) ∈ 𝐵) |
34 | 2, 3 | ringcl 19579 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑘) ∈ 𝐵 ∧ (𝑘𝐼𝑚) ∈ 𝐵) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) ∈ 𝐵) |
35 | 22, 28, 33, 34 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) ∈ 𝐵) |
36 | 35 | fmpttd 6932 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))):𝑀⟶𝐵) |
37 | | simp2 1139 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → 𝑘 ∈ 𝑀) |
38 | 32 | 3adant3 1134 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → 𝑚 ∈ 𝑀) |
39 | 2, 4, 12, 13, 14, 8 | mat1comp 21337 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀) → (𝑘𝐼𝑚) = if(𝑘 = 𝑚, 1 , 0 )) |
40 | 37, 38, 39 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → (𝑘𝐼𝑚) = if(𝑘 = 𝑚, 1 , 0 )) |
41 | | ifnefalse 4451 |
. . . . . . . . . 10
⊢ (𝑘 ≠ 𝑚 → if(𝑘 = 𝑚, 1 , 0 ) = 0 ) |
42 | 41 | 3ad2ant3 1137 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → if(𝑘 = 𝑚, 1 , 0 ) = 0 ) |
43 | 40, 42 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → (𝑘𝐼𝑚) = 0 ) |
44 | 43 | oveq2d 7229 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = ((𝑙𝑋𝑘)(.r‘𝑅) 0 )) |
45 | 2, 3, 13 | ringrz 19606 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑘) ∈ 𝐵) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) |
46 | 22, 28, 45 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) |
47 | 46 | 3adant3 1134 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) |
48 | 44, 47 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = 0 ) |
49 | 48, 9 | suppsssn 7943 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) supp 0 ) ⊆ {𝑚}) |
50 | 2, 13, 21, 9, 18, 36, 49 | gsumpt 19347 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑅 Σg (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))) = ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚)) |
51 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑙𝑋𝑘) = (𝑙𝑋𝑚)) |
52 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑘𝐼𝑚) = (𝑚𝐼𝑚)) |
53 | 51, 52 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) |
54 | | eqid 2737 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) = (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) |
55 | | ovex 7246 |
. . . . . . 7
⊢ ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) ∈ V |
56 | 53, 54, 55 | fvmpt 6818 |
. . . . . 6
⊢ (𝑚 ∈ 𝑀 → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) |
57 | 56 | ad2antll 729 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) |
58 | | equequ1 2033 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑚 → (𝑖 = 𝑗 ↔ 𝑚 = 𝑗)) |
59 | 58 | ifbid 4462 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → if(𝑖 = 𝑗, 1 , 0 ) = if(𝑚 = 𝑗, 1 , 0 )) |
60 | | equequ2 2034 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (𝑚 = 𝑗 ↔ 𝑚 = 𝑚)) |
61 | 60 | ifbid 4462 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → if(𝑚 = 𝑗, 1 , 0 ) = if(𝑚 = 𝑚, 1 , 0 )) |
62 | | eqid 2737 |
. . . . . . . . . . 11
⊢ 𝑚 = 𝑚 |
63 | 62 | iftruei 4446 |
. . . . . . . . . 10
⊢ if(𝑚 = 𝑚, 1 , 0 ) = 1 |
64 | 61, 63 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → if(𝑚 = 𝑗, 1 , 0 ) = 1 ) |
65 | 12 | fvexi 6731 |
. . . . . . . . 9
⊢ 1 ∈
V |
66 | 59, 64, 14, 65 | ovmpo 7369 |
. . . . . . . 8
⊢ ((𝑚 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀) → (𝑚𝐼𝑚) = 1 ) |
67 | 66 | anidms 570 |
. . . . . . 7
⊢ (𝑚 ∈ 𝑀 → (𝑚𝐼𝑚) = 1 ) |
68 | 67 | oveq2d 7229 |
. . . . . 6
⊢ (𝑚 ∈ 𝑀 → ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅) 1 )) |
69 | 68 | ad2antll 729 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅) 1 )) |
70 | 24 | fovrnda 7379 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙𝑋𝑚) ∈ 𝐵) |
71 | 2, 3, 12 | ringridm 19590 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑚) ∈ 𝐵) → ((𝑙𝑋𝑚)(.r‘𝑅) 1 ) = (𝑙𝑋𝑚)) |
72 | 5, 70, 71 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑙𝑋𝑚)(.r‘𝑅) 1 ) = (𝑙𝑋𝑚)) |
73 | 57, 69, 72 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = (𝑙𝑋𝑚)) |
74 | 19, 50, 73 | 3eqtrd 2781 |
. . 3
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚)) |
75 | 74 | ralrimivva 3112 |
. 2
⊢ (𝜑 → ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚)) |
76 | 2, 4, 1, 6, 8, 8, 10, 15 | mamucl 21298 |
. . . . 5
⊢ (𝜑 → (𝑋𝐹𝐼) ∈ (𝐵 ↑m (𝑁 × 𝑀))) |
77 | | elmapi 8530 |
. . . . 5
⊢ ((𝑋𝐹𝐼) ∈ (𝐵 ↑m (𝑁 × 𝑀)) → (𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵) |
78 | 76, 77 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵) |
79 | 78 | ffnd 6546 |
. . 3
⊢ (𝜑 → (𝑋𝐹𝐼) Fn (𝑁 × 𝑀)) |
80 | 24 | ffnd 6546 |
. . 3
⊢ (𝜑 → 𝑋 Fn (𝑁 × 𝑀)) |
81 | | eqfnov2 7340 |
. . 3
⊢ (((𝑋𝐹𝐼) Fn (𝑁 × 𝑀) ∧ 𝑋 Fn (𝑁 × 𝑀)) → ((𝑋𝐹𝐼) = 𝑋 ↔ ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚))) |
82 | 79, 80, 81 | syl2anc 587 |
. 2
⊢ (𝜑 → ((𝑋𝐹𝐼) = 𝑋 ↔ ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚))) |
83 | 75, 82 | mpbird 260 |
1
⊢ (𝜑 → (𝑋𝐹𝐼) = 𝑋) |