Metamath Proof Explorer

Theorem pwssub

Description: Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015)

Ref Expression
Hypotheses pwsgrp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsinvg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwssub.m ⊢ 𝑀 = ( -g ‘ 𝑅 )
pwssub.n ⊢ − = ( -g ‘ 𝑌 )
Assertion pwssub ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ∘f 𝑀 𝐺 ) )

Proof

Step Hyp Ref Expression
1 pwsgrp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsinvg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwssub.m ⊢ 𝑀 = ( -g ‘ 𝑅 )
4 pwssub.n ⊢ − = ( -g ‘ 𝑌 )
5 simplr ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 simpll ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝑅 ∈ Grp )
8 simprl ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐵 )
9 1 6 2 7 5 8 pwselbas ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
10 9 ffvelrnda ⊢ ( ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
11 fvexd ⊢ ( ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ V )
12 9 feqmptd ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
13 simprr ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐺 ∈ 𝐵 )
14 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
15 eqid ⊢ ( invg ‘ 𝑌 ) = ( invg ‘ 𝑌 )
16 1 2 14 15 pwsinvg ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) = ( ( invg ‘ 𝑅 ) ∘ 𝐺 ) )
17 7 5 13 16 syl3anc ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) = ( ( invg ‘ 𝑅 ) ∘ 𝐺 ) )
18 1 6 2 7 5 13 pwselbas ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐺 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
19 18 ffvelrnda ⊢ ( ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
20 18 feqmptd ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐺 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 ‘ 𝑥 ) ) )
21 6 14 grpinvf ⊢ ( 𝑅 ∈ Grp → ( invg ‘ 𝑅 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
22 21 ad2antrr ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( invg ‘ 𝑅 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
23 22 feqmptd ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( invg ‘ 𝑅 ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) ) )
24 fveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑦 ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) )
25 19 20 23 24 fmptco ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( invg ‘ 𝑅 ) ∘ 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
26 17 25 eqtrd ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
27 5 10 11 12 26 offval2 ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 ∘f ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
28 1 pwsgrp ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ Grp )
29 2 15 grpinvcl ⊢ ( ( 𝑌 ∈ Grp ∧ 𝐺 ∈ 𝐵 ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
30 28 13 29 syl2an2r ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ∈ 𝐵 )
31 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
32 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
33 1 2 7 5 8 30 31 32 pwsplusgval ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) = ( 𝐹 ∘f ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
34 6 31 14 3 grpsubval ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
35 10 19 34 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
36 35 mpteq2dva ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
37 27 33 36 3eqtr4d ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐺 ‘ 𝑥 ) ) ) )
38 2 32 15 4 grpsubval ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
39 38 adantl ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ( +g ‘ 𝑌 ) ( ( invg ‘ 𝑌 ) ‘ 𝐺 ) ) )
40 5 10 19 12 20 offval2 ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 ∘f 𝑀 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑀 ( 𝐺 ‘ 𝑥 ) ) ) )
41 37 39 40 3eqtr4d ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝐹 − 𝐺 ) = ( 𝐹 ∘f 𝑀 𝐺 ) )