| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) |
| 2 | | simp2 1138 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
| 3 | | fvexd 6921 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (Scalar‘𝑅) ∈ V) |
| 4 | | simp1 1137 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Grp) |
| 5 | | fconst6g 6797 |
. . . . 5
⊢ (𝑅 ∈ Grp → (𝐼 × {𝑅}):𝐼⟶Grp) |
| 6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝐼 × {𝑅}):𝐼⟶Grp) |
| 7 | | eqid 2737 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 8 | | eqid 2737 |
. . . 4
⊢
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) =
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 9 | | simp3 1139 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
| 10 | | pwsinvg.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑌) |
| 11 | | pwsgrp.y |
. . . . . . . . 9
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
| 12 | | eqid 2737 |
. . . . . . . . 9
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 13 | 11, 12 | pwsval 17531 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 14 | 13 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 15 | 14 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (Base‘𝑌) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 16 | 10, 15 | eqtrid 2789 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝐵 = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 17 | 9, 16 | eleqtrd 2843 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 18 | 1, 2, 3, 6, 7, 8, 17 | prdsinvgd 19069 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) →
((invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))‘𝑋) = (𝑥 ∈ 𝐼 ↦ ((invg‘((𝐼 × {𝑅})‘𝑥))‘(𝑋‘𝑥)))) |
| 19 | | fvconst2g 7222 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
| 20 | 4, 19 | sylan 580 |
. . . . . . 7
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
| 21 | 20 | fveq2d 6910 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (invg‘((𝐼 × {𝑅})‘𝑥)) = (invg‘𝑅)) |
| 22 | | pwsinvg.m |
. . . . . 6
⊢ 𝑀 = (invg‘𝑅) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . 5
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (invg‘((𝐼 × {𝑅})‘𝑥)) = 𝑀) |
| 24 | 23 | fveq1d 6908 |
. . . 4
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → ((invg‘((𝐼 × {𝑅})‘𝑥))‘(𝑋‘𝑥)) = (𝑀‘(𝑋‘𝑥))) |
| 25 | 24 | mpteq2dva 5242 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((invg‘((𝐼 × {𝑅})‘𝑥))‘(𝑋‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑀‘(𝑋‘𝑥)))) |
| 26 | 18, 25 | eqtrd 2777 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) →
((invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))‘𝑋) = (𝑥 ∈ 𝐼 ↦ (𝑀‘(𝑋‘𝑥)))) |
| 27 | | pwsinvg.n |
. . . 4
⊢ 𝑁 = (invg‘𝑌) |
| 28 | 14 | fveq2d 6910 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (invg‘𝑌) =
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 29 | 27, 28 | eqtrid 2789 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑁 =
(invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 30 | 29 | fveq1d 6908 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) =
((invg‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))‘𝑋)) |
| 31 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 32 | 11, 31, 10, 4, 2, 9 | pwselbas 17534 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋:𝐼⟶(Base‘𝑅)) |
| 33 | 32 | ffvelcdmda 7104 |
. . 3
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
| 34 | 32 | feqmptd 6977 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑋 = (𝑥 ∈ 𝐼 ↦ (𝑋‘𝑥))) |
| 35 | 31, 22 | grpinvf 19004 |
. . . . 5
⊢ (𝑅 ∈ Grp → 𝑀:(Base‘𝑅)⟶(Base‘𝑅)) |
| 36 | 4, 35 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑀:(Base‘𝑅)⟶(Base‘𝑅)) |
| 37 | 36 | feqmptd 6977 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → 𝑀 = (𝑦 ∈ (Base‘𝑅) ↦ (𝑀‘𝑦))) |
| 38 | | fveq2 6906 |
. . 3
⊢ (𝑦 = (𝑋‘𝑥) → (𝑀‘𝑦) = (𝑀‘(𝑋‘𝑥))) |
| 39 | 33, 34, 37, 38 | fmptco 7149 |
. 2
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑀 ∘ 𝑋) = (𝑥 ∈ 𝐼 ↦ (𝑀‘(𝑋‘𝑥)))) |
| 40 | 26, 30, 39 | 3eqtr4d 2787 |
1
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = (𝑀 ∘ 𝑋)) |