Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . 4
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐼 ∈ 𝑉) |
2 | | pwsgrp.y |
. . . . . 6
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
3 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | pwsinvg.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑌) |
5 | | simpll 786 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝑅 ∈ Grp) |
6 | | simprl 790 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐹 ∈ 𝐵) |
7 | 2, 3, 4, 5, 1, 6 | pwselbas 15972 |
. . . . 5
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐹:𝐼⟶(Base‘𝑅)) |
8 | 7 | ffvelrnda 6267 |
. . . 4
⊢ ((((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝐹‘𝑥) ∈ (Base‘𝑅)) |
9 | | fvex 6113 |
. . . . 5
⊢
((invg‘𝑅)‘(𝐺‘𝑥)) ∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ ((((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((invg‘𝑅)‘(𝐺‘𝑥)) ∈ V) |
11 | 7 | feqmptd 6159 |
. . . 4
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐹 = (𝑥 ∈ 𝐼 ↦ (𝐹‘𝑥))) |
12 | | simprr 792 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐺 ∈ 𝐵) |
13 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝑅) = (invg‘𝑅) |
14 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝑌) = (invg‘𝑌) |
15 | 2, 4, 13, 14 | pwsinvg 17351 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵) → ((invg‘𝑌)‘𝐺) = ((invg‘𝑅) ∘ 𝐺)) |
16 | 5, 1, 12, 15 | syl3anc 1318 |
. . . . 5
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((invg‘𝑌)‘𝐺) = ((invg‘𝑅) ∘ 𝐺)) |
17 | 2, 3, 4, 5, 1, 12 | pwselbas 15972 |
. . . . . . 7
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐺:𝐼⟶(Base‘𝑅)) |
18 | 17 | ffvelrnda 6267 |
. . . . . 6
⊢ ((((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ (Base‘𝑅)) |
19 | 17 | feqmptd 6159 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥))) |
20 | 3, 13 | grpinvf 17289 |
. . . . . . . 8
⊢ (𝑅 ∈ Grp →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
21 | 20 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
22 | 21 | feqmptd 6159 |
. . . . . 6
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (invg‘𝑅) = (𝑦 ∈ (Base‘𝑅) ↦ ((invg‘𝑅)‘𝑦))) |
23 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = (𝐺‘𝑥) → ((invg‘𝑅)‘𝑦) = ((invg‘𝑅)‘(𝐺‘𝑥))) |
24 | 18, 19, 22, 23 | fmptco 6303 |
. . . . 5
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((invg‘𝑅) ∘ 𝐺) = (𝑥 ∈ 𝐼 ↦ ((invg‘𝑅)‘(𝐺‘𝑥)))) |
25 | 16, 24 | eqtrd 2644 |
. . . 4
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((invg‘𝑌)‘𝐺) = (𝑥 ∈ 𝐼 ↦ ((invg‘𝑅)‘(𝐺‘𝑥)))) |
26 | 1, 8, 10, 11, 25 | offval2 6812 |
. . 3
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 ∘𝑓
(+g‘𝑅)((invg‘𝑌)‘𝐺)) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(+g‘𝑅)((invg‘𝑅)‘(𝐺‘𝑥))))) |
27 | 2 | pwsgrp 17350 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Grp) |
28 | 27 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝑌 ∈ Grp) |
29 | 4, 14 | grpinvcl 17290 |
. . . . 5
⊢ ((𝑌 ∈ Grp ∧ 𝐺 ∈ 𝐵) → ((invg‘𝑌)‘𝐺) ∈ 𝐵) |
30 | 28, 12, 29 | syl2anc 691 |
. . . 4
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((invg‘𝑌)‘𝐺) ∈ 𝐵) |
31 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
32 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑌) = (+g‘𝑌) |
33 | 2, 4, 5, 1, 6, 30,
31, 32 | pwsplusgval 15973 |
. . 3
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹(+g‘𝑌)((invg‘𝑌)‘𝐺)) = (𝐹 ∘𝑓
(+g‘𝑅)((invg‘𝑌)‘𝐺))) |
34 | | pwssub.m |
. . . . . 6
⊢ 𝑀 = (-g‘𝑅) |
35 | 3, 31, 13, 34 | grpsubval 17288 |
. . . . 5
⊢ (((𝐹‘𝑥) ∈ (Base‘𝑅) ∧ (𝐺‘𝑥) ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑀(𝐺‘𝑥)) = ((𝐹‘𝑥)(+g‘𝑅)((invg‘𝑅)‘(𝐺‘𝑥)))) |
36 | 8, 18, 35 | syl2anc 691 |
. . . 4
⊢ ((((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝐹‘𝑥)𝑀(𝐺‘𝑥)) = ((𝐹‘𝑥)(+g‘𝑅)((invg‘𝑅)‘(𝐺‘𝑥)))) |
37 | 36 | mpteq2dva 4672 |
. . 3
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝑀(𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(+g‘𝑅)((invg‘𝑅)‘(𝐺‘𝑥))))) |
38 | 26, 33, 37 | 3eqtr4d 2654 |
. 2
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹(+g‘𝑌)((invg‘𝑌)‘𝐺)) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝑀(𝐺‘𝑥)))) |
39 | | pwssub.n |
. . . 4
⊢ − =
(-g‘𝑌) |
40 | 4, 32, 14, 39 | grpsubval 17288 |
. . 3
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 − 𝐺) = (𝐹(+g‘𝑌)((invg‘𝑌)‘𝐺))) |
41 | 40 | adantl 481 |
. 2
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 − 𝐺) = (𝐹(+g‘𝑌)((invg‘𝑌)‘𝐺))) |
42 | 1, 8, 18, 11, 19 | offval2 6812 |
. 2
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 ∘𝑓 𝑀𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝑀(𝐺‘𝑥)))) |
43 | 38, 41, 42 | 3eqtr4d 2654 |
1
⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 − 𝐺) = (𝐹 ∘𝑓 𝑀𝐺)) |