Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | marep01ma.0 |
. . 3
⊢ 0 =
(0g‘𝑅) |
3 | | eqid 2610 |
. . 3
⊢
(Cntz‘𝑅) =
(Cntz‘𝑅) |
4 | | marep01ma.r |
. . . . 5
⊢ 𝑅 ∈ CRing |
5 | | crngring 18381 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
6 | | ringmnd 18379 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
7 | 4, 5, 6 | mp2b 10 |
. . . 4
⊢ 𝑅 ∈ Mnd |
8 | 7 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → 𝑅 ∈ Mnd) |
9 | | smadiadetlem.w |
. . . 4
⊢ 𝑊 =
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
10 | | fvex 6113 |
. . . . 5
⊢
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ∈ V |
11 | 10 | a1i 11 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ∈ V) |
12 | 9, 11 | syl5eqel 2692 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → 𝑊 ∈ V) |
13 | | marep01ma.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
14 | | marep01ma.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
15 | | marep01ma.1 |
. . . 4
⊢ 1 =
(1r‘𝑅) |
16 | | smadiadetlem.p |
. . . 4
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
17 | | smadiadetlem.g |
. . . 4
⊢ 𝐺 = (mulGrp‘𝑅) |
18 | | madetminlem.y |
. . . 4
⊢ 𝑌 = (ℤRHom‘𝑅) |
19 | | madetminlem.s |
. . . 4
⊢ 𝑆 = (pmSgn‘𝑁) |
20 | | madetminlem.t |
. . . 4
⊢ · =
(.r‘𝑅) |
21 | | smadiadetlem.z |
. . . 4
⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) |
22 | 13, 14, 4, 2, 15, 16, 17, 18, 19, 20, 9, 21 | smadiadetlem3lem1 20291 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))):𝑊⟶(Base‘𝑅)) |
23 | 13, 14, 4, 2, 15, 16, 17, 18, 19, 20, 9, 21 | smadiadetlem3lem2 20292 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → ran (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ⊆ ((Cntz‘𝑅)‘ran (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) |
24 | | eqid 2610 |
. . . 4
⊢ (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) = (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) |
25 | 13, 14 | matrcl 20037 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
26 | 25 | simpld 474 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → 𝑁 ∈ Fin) |
27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → 𝑁 ∈ Fin) |
28 | | diffi 8077 |
. . . . . 6
⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝐾}) ∈ Fin) |
29 | | eqid 2610 |
. . . . . . 7
⊢
(SymGrp‘(𝑁
∖ {𝐾})) =
(SymGrp‘(𝑁 ∖
{𝐾})) |
30 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
31 | 29, 30 | symgbasfi 17629 |
. . . . . 6
⊢ ((𝑁 ∖ {𝐾}) ∈ Fin →
(Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ∈ Fin) |
32 | 27, 28, 31 | 3syl 18 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) ∈ Fin) |
33 | 9, 32 | syl5eqel 2692 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → 𝑊 ∈ Fin) |
34 | | ovex 6577 |
. . . . 5
⊢ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))) ∈ V |
35 | 34 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑊) → (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))) ∈ V) |
36 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
37 | 2, 36 | eqeltri 2684 |
. . . . 5
⊢ 0 ∈
V |
38 | 37 | a1i 11 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → 0 ∈ V) |
39 | 24, 33, 35, 38 | fsuppmptdm 8169 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) finSupp 0 ) |
40 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑞 = 𝑝 → (𝑞‘𝐾) = (𝑝‘𝐾)) |
41 | 40 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑞 = 𝑝 → ((𝑞‘𝐾) = 𝐾 ↔ (𝑝‘𝐾) = 𝐾)) |
42 | 41 | cbvrabv 3172 |
. . . . 5
⊢ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} = {𝑝 ∈ 𝑃 ∣ (𝑝‘𝐾) = 𝐾} |
43 | | eqid 2610 |
. . . . 5
⊢ (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾}))) = (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾}))) |
44 | 16, 42, 9, 43 | symgfixf1o 17683 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾}))):{𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}–1-1-onto→𝑊) |
45 | 26, 44 | sylan 487 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾}))):{𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}–1-1-onto→𝑊) |
46 | 1, 2, 3, 8, 12, 22, 23, 39, 45 | gsumzf1o 18136 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) = (𝑅 Σg ((𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ∘ (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾})))))) |
47 | | eqid 2610 |
. . . . . . 7
⊢ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} |
48 | | eqid 2610 |
. . . . . . 7
⊢ (𝑁 ∖ {𝐾}) = (𝑁 ∖ {𝐾}) |
49 | 16, 47, 9, 48 | symgfixelsi 17678 |
. . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → (𝑝 ↾ (𝑁 ∖ {𝐾})) ∈ 𝑊) |
50 | 49 | adantll 746 |
. . . . 5
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → (𝑝 ↾ (𝑁 ∖ {𝐾})) ∈ 𝑊) |
51 | | eqidd 2611 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾}))) = (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾})))) |
52 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑝 = 𝑦 → ((𝑌 ∘ 𝑍)‘𝑝) = ((𝑌 ∘ 𝑍)‘𝑦)) |
53 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑦 → (𝑝‘𝑛) = (𝑦‘𝑛)) |
54 | 53 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑦 → (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛))) |
55 | 54 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑝 = 𝑦 → (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))) = (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛)))) |
56 | 55 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑝 = 𝑦 → (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))) = (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛))))) |
57 | 52, 56 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑝 = 𝑦 → (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))) = (((𝑌 ∘ 𝑍)‘𝑦)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛)))))) |
58 | 57 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) = (𝑦 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑦)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛)))))) |
59 | 58 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) = (𝑦 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑦)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛))))))) |
60 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) → ((𝑌 ∘ 𝑍)‘𝑦) = ((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾})))) |
61 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) → (𝑦‘𝑛) = ((𝑝 ↾ (𝑁 ∖ {𝐾}))‘𝑛)) |
62 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑝 ↾ (𝑁 ∖ {𝐾}))‘𝑛) = (𝑝‘𝑛)) |
63 | 61, 62 | sylan9eq 2664 |
. . . . . . . . 9
⊢ ((𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑦‘𝑛) = (𝑝‘𝑛)) |
64 | 63 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))) |
65 | 64 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) → (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛))) = (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))) |
66 | 65 | oveq2d 6565 |
. . . . . 6
⊢ (𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) → (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛)))) = (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))) |
67 | 60, 66 | oveq12d 6567 |
. . . . 5
⊢ (𝑦 = (𝑝 ↾ (𝑁 ∖ {𝐾})) → (((𝑌 ∘ 𝑍)‘𝑦)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑦‘𝑛))))) = (((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾})))(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) |
68 | 50, 51, 59, 67 | fmptco 6303 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → ((𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ∘ (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾})))) = (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾})))(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) |
69 | 16, 19, 21, 18 | zrhcopsgndif 19768 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → ((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾}))) = ((𝑌 ∘ 𝑆)‘𝑝))) |
70 | 26, 69 | sylan 487 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → ((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾}))) = ((𝑌 ∘ 𝑆)‘𝑝))) |
71 | 70 | imp 444 |
. . . . . 6
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾}))) = ((𝑌 ∘ 𝑆)‘𝑝)) |
72 | 71 | oveq1d 6564 |
. . . . 5
⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → (((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾})))(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))) = (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) |
73 | 72 | mpteq2dva 4672 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑍)‘(𝑝 ↾ (𝑁 ∖ {𝐾})))(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) = (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) |
74 | 68, 73 | eqtrd 2644 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → ((𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ∘ (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾})))) = (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) |
75 | 74 | oveq2d 6565 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg ((𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ∘ (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (𝑝 ↾ (𝑁 ∖ {𝐾}))))) = (𝑅 Σg (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) |
76 | 46, 75 | eqtr2d 2645 |
1
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) = (𝑅 Σg (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) |