Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) |
2 | | simp2 1055 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
3 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑅)
∈ V |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (Scalar‘𝑅) ∈ V) |
5 | | simp1 1054 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Grp) |
6 | | fconst6g 6007 |
. . . . 5
⊢ (𝑅 ∈ Grp → (𝐼 × {𝑅}):𝐼⟶Grp) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝐼 × {𝑅}):𝐼⟶Grp) |
8 | | eqid 2610 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
9 | | eqid 2610 |
. . . 4
⊢
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) =
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
10 | | simp3 1056 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
11 | | pwsinvg.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑌) |
12 | | pwsgrp.y |
. . . . . . . . 9
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
14 | 12, 13 | pwsval 15969 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
15 | 14 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
16 | 15 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (Base‘𝑌) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
17 | 11, 16 | syl5eq 2656 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝐵 = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
18 | 10, 17 | eleqtrd 2690 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
19 | 1, 2, 4, 7, 8, 9, 18 | prdsinvgd 17349 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) →
((invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))‘𝑋) = (𝑥 ∈ 𝐼 ↦ ((invg‘((𝐼 × {𝑅})‘𝑥))‘(𝑋‘𝑥)))) |
20 | | fvconst2g 6372 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
21 | 5, 20 | sylan 487 |
. . . . . . 7
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
22 | 21 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (invg‘((𝐼 × {𝑅})‘𝑥)) = (invg‘𝑅)) |
23 | | pwsinvg.m |
. . . . . 6
⊢ 𝑀 = (invg‘𝑅) |
24 | 22, 23 | syl6eqr 2662 |
. . . . 5
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (invg‘((𝐼 × {𝑅})‘𝑥)) = 𝑀) |
25 | 24 | fveq1d 6105 |
. . . 4
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((invg‘((𝐼 × {𝑅})‘𝑥))‘(𝑋‘𝑥)) = (𝑀‘(𝑋‘𝑥))) |
26 | 25 | mpteq2dva 4672 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((invg‘((𝐼 × {𝑅})‘𝑥))‘(𝑋‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑀‘(𝑋‘𝑥)))) |
27 | 19, 26 | eqtrd 2644 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) →
((invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))‘𝑋) = (𝑥 ∈ 𝐼 ↦ (𝑀‘(𝑋‘𝑥)))) |
28 | | pwsinvg.n |
. . . 4
⊢ 𝑁 = (invg‘𝑌) |
29 | 15 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (invg‘𝑌) =
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
30 | 28, 29 | syl5eq 2656 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑁 =
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
31 | 30 | fveq1d 6105 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) =
((invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))‘𝑋)) |
32 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
33 | 12, 32, 11, 5, 2, 10 | pwselbas 15972 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋:𝐼⟶(Base‘𝑅)) |
34 | 33 | ffvelrnda 6267 |
. . 3
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
35 | 33 | feqmptd 6159 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋 = (𝑥 ∈ 𝐼 ↦ (𝑋‘𝑥))) |
36 | 32, 23 | grpinvf 17289 |
. . . . 5
⊢ (𝑅 ∈ Grp → 𝑀:(Base‘𝑅)⟶(Base‘𝑅)) |
37 | 5, 36 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑀:(Base‘𝑅)⟶(Base‘𝑅)) |
38 | 37 | feqmptd 6159 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑀 = (𝑦 ∈ (Base‘𝑅) ↦ (𝑀‘𝑦))) |
39 | | fveq2 6103 |
. . 3
⊢ (𝑦 = (𝑋‘𝑥) → (𝑀‘𝑦) = (𝑀‘(𝑋‘𝑥))) |
40 | 34, 35, 38, 39 | fmptco 6303 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑀 ∘ 𝑋) = (𝑥 ∈ 𝐼 ↦ (𝑀‘(𝑋‘𝑥)))) |
41 | 27, 31, 40 | 3eqtr4d 2654 |
1
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = (𝑀 ∘ 𝑋)) |