Step | Hyp | Ref
| Expression |
1 | | mamurid.f |
. . . . 5
⊢ 𝐹 = (𝑅 maMul 〈𝑁, 𝑀, 𝑀〉) |
2 | | mamumat1cl.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
3 | | eqid 2610 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | mamumat1cl.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑅 ∈ Ring) |
6 | | mamulid.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ Fin) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑁 ∈ Fin) |
8 | | mamumat1cl.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Fin) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑀 ∈ Fin) |
10 | | mamurid.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑀))) |
11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑋 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑀))) |
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 20064 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑀))) |
16 | 15 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝐼 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑀))) |
17 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑙 ∈ 𝑁) |
18 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑚 ∈ 𝑀) |
19 | 1, 2, 3, 5, 7, 9, 9, 11, 16, 17, 18 | mamufv 20012 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙(𝑋𝐹𝐼)𝑚) = (𝑅 Σg (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))))) |
20 | | ringmnd 18379 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
21 | 5, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → 𝑅 ∈ Mnd) |
22 | 4 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑅 ∈ Ring) |
23 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑𝑚 (𝑁 × 𝑀)) → 𝑋:(𝑁 × 𝑀)⟶𝐵) |
24 | 10, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:(𝑁 × 𝑀)⟶𝐵) |
25 | 24 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑋:(𝑁 × 𝑀)⟶𝐵) |
26 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑙 ∈ 𝑁) |
27 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑘 ∈ 𝑀) |
28 | 25, 26, 27 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → (𝑙𝑋𝑘) ∈ 𝐵) |
29 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑀)) → 𝐼:(𝑀 × 𝑀)⟶𝐵) |
30 | 15, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼:(𝑀 × 𝑀)⟶𝐵) |
31 | 30 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝐼:(𝑀 × 𝑀)⟶𝐵) |
32 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → 𝑚 ∈ 𝑀) |
33 | 31, 27, 32 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → (𝑘𝐼𝑚) ∈ 𝐵) |
34 | 2, 3 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑘) ∈ 𝐵 ∧ (𝑘𝐼𝑚) ∈ 𝐵) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) ∈ 𝐵) |
35 | 22, 28, 33, 34 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) ∈ 𝐵) |
36 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) = (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) |
37 | 35, 36 | fmptd 6292 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))):𝑀⟶𝐵) |
38 | | simp2 1055 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → 𝑘 ∈ 𝑀) |
39 | 32 | 3adant3 1074 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → 𝑚 ∈ 𝑀) |
40 | 2, 4, 12, 13, 14, 8 | mat1comp 20065 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀) → (𝑘𝐼𝑚) = if(𝑘 = 𝑚, 1 , 0 )) |
41 | 38, 39, 40 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → (𝑘𝐼𝑚) = if(𝑘 = 𝑚, 1 , 0 )) |
42 | | ifnefalse 4048 |
. . . . . . . . . 10
⊢ (𝑘 ≠ 𝑚 → if(𝑘 = 𝑚, 1 , 0 ) = 0 ) |
43 | 42 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → if(𝑘 = 𝑚, 1 , 0 ) = 0 ) |
44 | 41, 43 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → (𝑘𝐼𝑚) = 0 ) |
45 | 44 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = ((𝑙𝑋𝑘)(.r‘𝑅) 0 )) |
46 | 2, 3, 13 | ringrz 18411 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑘) ∈ 𝐵) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) |
47 | 22, 28, 46 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) |
48 | 47 | 3adant3 1074 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅) 0 ) = 0 ) |
49 | 45, 48 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) ∧ 𝑘 ∈ 𝑀 ∧ 𝑘 ≠ 𝑚) → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = 0 ) |
50 | 49, 9 | suppsssn 7217 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚))) supp 0 ) ⊆ {𝑚}) |
51 | 2, 13, 21, 9, 18, 37, 50 | gsumpt 18184 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑅 Σg (𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))) = ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚)) |
52 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑙𝑋𝑘) = (𝑙𝑋𝑚)) |
53 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑘𝐼𝑚) = (𝑚𝐼𝑚)) |
54 | 52, 53 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) |
55 | | ovex 6577 |
. . . . . . 7
⊢ ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) ∈ V |
56 | 54, 36, 55 | fvmpt 6191 |
. . . . . 6
⊢ (𝑚 ∈ 𝑀 → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) |
57 | 56 | ad2antll 761 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚))) |
58 | | equequ1 1939 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑚 → (𝑖 = 𝑗 ↔ 𝑚 = 𝑗)) |
59 | 58 | ifbid 4058 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → if(𝑖 = 𝑗, 1 , 0 ) = if(𝑚 = 𝑗, 1 , 0 )) |
60 | | equequ2 1940 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (𝑚 = 𝑗 ↔ 𝑚 = 𝑚)) |
61 | 60 | ifbid 4058 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → if(𝑚 = 𝑗, 1 , 0 ) = if(𝑚 = 𝑚, 1 , 0 )) |
62 | | eqid 2610 |
. . . . . . . . . . 11
⊢ 𝑚 = 𝑚 |
63 | 62 | iftruei 4043 |
. . . . . . . . . 10
⊢ if(𝑚 = 𝑚, 1 , 0 ) = 1 |
64 | 61, 63 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → if(𝑚 = 𝑗, 1 , 0 ) = 1 ) |
65 | | fvex 6113 |
. . . . . . . . . 10
⊢
(1r‘𝑅) ∈ V |
66 | 12, 65 | eqeltri 2684 |
. . . . . . . . 9
⊢ 1 ∈
V |
67 | 59, 64, 14, 66 | ovmpt2 6694 |
. . . . . . . 8
⊢ ((𝑚 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀) → (𝑚𝐼𝑚) = 1 ) |
68 | 67 | anidms 675 |
. . . . . . 7
⊢ (𝑚 ∈ 𝑀 → (𝑚𝐼𝑚) = 1 ) |
69 | 68 | oveq2d 6565 |
. . . . . 6
⊢ (𝑚 ∈ 𝑀 → ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅) 1 )) |
70 | 69 | ad2antll 761 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑙𝑋𝑚)(.r‘𝑅)(𝑚𝐼𝑚)) = ((𝑙𝑋𝑚)(.r‘𝑅) 1 )) |
71 | 24 | fovrnda 6703 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙𝑋𝑚) ∈ 𝐵) |
72 | 2, 3, 12 | ringridm 18395 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑙𝑋𝑚) ∈ 𝐵) → ((𝑙𝑋𝑚)(.r‘𝑅) 1 ) = (𝑙𝑋𝑚)) |
73 | 5, 71, 72 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑙𝑋𝑚)(.r‘𝑅) 1 ) = (𝑙𝑋𝑚)) |
74 | 57, 70, 73 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → ((𝑘 ∈ 𝑀 ↦ ((𝑙𝑋𝑘)(.r‘𝑅)(𝑘𝐼𝑚)))‘𝑚) = (𝑙𝑋𝑚)) |
75 | 19, 51, 74 | 3eqtrd 2648 |
. . 3
⊢ ((𝜑 ∧ (𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀)) → (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚)) |
76 | 75 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚)) |
77 | 2, 4, 1, 6, 8, 8, 10, 15 | mamucl 20026 |
. . . . 5
⊢ (𝜑 → (𝑋𝐹𝐼) ∈ (𝐵 ↑𝑚 (𝑁 × 𝑀))) |
78 | | elmapi 7765 |
. . . . 5
⊢ ((𝑋𝐹𝐼) ∈ (𝐵 ↑𝑚 (𝑁 × 𝑀)) → (𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵) |
79 | 77, 78 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵) |
80 | | ffn 5958 |
. . . 4
⊢ ((𝑋𝐹𝐼):(𝑁 × 𝑀)⟶𝐵 → (𝑋𝐹𝐼) Fn (𝑁 × 𝑀)) |
81 | 79, 80 | syl 17 |
. . 3
⊢ (𝜑 → (𝑋𝐹𝐼) Fn (𝑁 × 𝑀)) |
82 | | ffn 5958 |
. . . 4
⊢ (𝑋:(𝑁 × 𝑀)⟶𝐵 → 𝑋 Fn (𝑁 × 𝑀)) |
83 | 24, 82 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 Fn (𝑁 × 𝑀)) |
84 | | eqfnov2 6665 |
. . 3
⊢ (((𝑋𝐹𝐼) Fn (𝑁 × 𝑀) ∧ 𝑋 Fn (𝑁 × 𝑀)) → ((𝑋𝐹𝐼) = 𝑋 ↔ ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚))) |
85 | 81, 83, 84 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑋𝐹𝐼) = 𝑋 ↔ ∀𝑙 ∈ 𝑁 ∀𝑚 ∈ 𝑀 (𝑙(𝑋𝐹𝐼)𝑚) = (𝑙𝑋𝑚))) |
86 | 76, 85 | mpbird 246 |
1
⊢ (𝜑 → (𝑋𝐹𝐼) = 𝑋) |