Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢ (𝑗 ∈ 𝑀, 𝑖 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))))) = (𝑗 ∈ 𝑀, 𝑖 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))))) |
2 | 1 | tposmpo 7959 |
. . 3
⊢ tpos
(𝑗 ∈ 𝑀, 𝑖 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))))) = (𝑖 ∈ 𝑃, 𝑗 ∈ 𝑀 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))))) |
3 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝜑) |
4 | | mamutpos.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ CRing) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝑅 ∈ CRing) |
6 | | mamutpos.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) |
7 | | elmapi 8460 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
8 | 3, 6, 7 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝑋:(𝑀 × 𝑁)⟶𝐵) |
9 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝑗 ∈ 𝑀) |
10 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
11 | 8, 9, 10 | fovrnd 7337 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → (𝑗𝑋𝑘) ∈ 𝐵) |
12 | | mamutpos.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃))) |
13 | | elmapi 8460 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)) → 𝑌:(𝑁 × 𝑃)⟶𝐵) |
14 | 3, 12, 13 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝑌:(𝑁 × 𝑃)⟶𝐵) |
15 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → 𝑖 ∈ 𝑃) |
16 | 14, 10, 15 | fovrnd 7337 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑌𝑖) ∈ 𝐵) |
17 | | mamutpos.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
18 | | eqid 2738 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 17, 18 | crngcom 19435 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑗𝑋𝑘) ∈ 𝐵 ∧ (𝑘𝑌𝑖) ∈ 𝐵) → ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖)) = ((𝑘𝑌𝑖)(.r‘𝑅)(𝑗𝑋𝑘))) |
20 | 5, 11, 16, 19 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖)) = ((𝑘𝑌𝑖)(.r‘𝑅)(𝑗𝑋𝑘))) |
21 | | ovtpos 7937 |
. . . . . . . 8
⊢ (𝑖tpos 𝑌𝑘) = (𝑘𝑌𝑖) |
22 | | ovtpos 7937 |
. . . . . . . 8
⊢ (𝑘tpos 𝑋𝑗) = (𝑗𝑋𝑘) |
23 | 21, 22 | oveq12i 7183 |
. . . . . . 7
⊢ ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗)) = ((𝑘𝑌𝑖)(.r‘𝑅)(𝑗𝑋𝑘)) |
24 | 20, 23 | eqtr4di 2791 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) ∧ 𝑘 ∈ 𝑁) → ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖)) = ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗))) |
25 | 24 | mpteq2dva 5126 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) → (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))) = (𝑘 ∈ 𝑁 ↦ ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗)))) |
26 | 25 | oveq2d 7187 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀) → (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖)))) = (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗))))) |
27 | 26 | mpoeq3dva 7246 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝑃, 𝑗 ∈ 𝑀 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))))) = (𝑖 ∈ 𝑃, 𝑗 ∈ 𝑀 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗)))))) |
28 | 2, 27 | syl5eq 2785 |
. 2
⊢ (𝜑 → tpos (𝑗 ∈ 𝑀, 𝑖 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖))))) = (𝑖 ∈ 𝑃, 𝑗 ∈ 𝑀 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗)))))) |
29 | | mamutpos.f |
. . . 4
⊢ 𝐹 = (𝑅 maMul 〈𝑀, 𝑁, 𝑃〉) |
30 | | mamutpos.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Fin) |
31 | | mamutpos.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) |
32 | | mamutpos.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ Fin) |
33 | 29, 17, 18, 4, 30, 31, 32, 6, 12 | mamuval 21140 |
. . 3
⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑗 ∈ 𝑀, 𝑖 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖)))))) |
34 | 33 | tposeqd 7925 |
. 2
⊢ (𝜑 → tpos (𝑋𝐹𝑌) = tpos (𝑗 ∈ 𝑀, 𝑖 ∈ 𝑃 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑗𝑋𝑘)(.r‘𝑅)(𝑘𝑌𝑖)))))) |
35 | | mamutpos.g |
. . 3
⊢ 𝐺 = (𝑅 maMul 〈𝑃, 𝑁, 𝑀〉) |
36 | | tposmap 21209 |
. . . 4
⊢ (𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)) → tpos 𝑌 ∈ (𝐵 ↑m (𝑃 × 𝑁))) |
37 | 12, 36 | syl 17 |
. . 3
⊢ (𝜑 → tpos 𝑌 ∈ (𝐵 ↑m (𝑃 × 𝑁))) |
38 | | tposmap 21209 |
. . . 4
⊢ (𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)) → tpos 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀))) |
39 | 6, 38 | syl 17 |
. . 3
⊢ (𝜑 → tpos 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀))) |
40 | 35, 17, 18, 4, 32, 31, 30, 37, 39 | mamuval 21140 |
. 2
⊢ (𝜑 → (tpos 𝑌𝐺tpos 𝑋) = (𝑖 ∈ 𝑃, 𝑗 ∈ 𝑀 ↦ (𝑅 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖tpos 𝑌𝑘)(.r‘𝑅)(𝑘tpos 𝑋𝑗)))))) |
41 | 28, 34, 40 | 3eqtr4d 2783 |
1
⊢ (𝜑 → tpos (𝑋𝐹𝑌) = (tpos 𝑌𝐺tpos 𝑋)) |