Metamath Proof Explorer

Theorem pwsinvg

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

Ref Expression
Hypotheses pwsgrp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsinvg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsinvg.m ⊢ 𝑀 = ( invg ‘ 𝑅 )
pwsinvg.n ⊢ 𝑁 = ( invg ‘ 𝑌 )
Assertion pwsinvg ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝑀 ∘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 pwsgrp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsinvg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwsinvg.m ⊢ 𝑀 = ( invg ‘ 𝑅 )
4 pwsinvg.n ⊢ 𝑁 = ( invg ‘ 𝑌 )
5 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
6 simp2 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
7 fvexd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( Scalar ‘ 𝑅 ) ∈ V )
8 simp1 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Grp )
9 fconst6g ⊢ ( 𝑅 ∈ Grp → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Grp )
10 8 9 syl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Grp )
11 eqid ⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
12 eqid ⊢ ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
13 simp3 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
14 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
15 1 14 pwsval ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
16 15 3adant3 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
17 16 fveq2d ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
18 2 17 syl5eq ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝐵 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
19 13 18 eleqtrd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
20 5 6 7 10 11 12 19 prdsinvgd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
21 fvconst2g ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
22 8 21 sylan ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
23 22 fveq2d ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( invg ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( invg ‘ 𝑅 ) )
24 23 3 eqtr4di ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( invg ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = 𝑀 )
25 24 fveq1d ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( invg ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝑋 ‘ 𝑥 ) ) )
26 25 mpteq2dva ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑀 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
27 20 26 eqtrd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑀 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
28 16 fveq2d ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( invg ‘ 𝑌 ) = ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
29 4 28 syl5eq ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑁 = ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
30 29 fveq1d ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = ( ( invg ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ‘ 𝑋 ) )
31 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32 1 31 2 8 6 13 pwselbas ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
33 32 ffvelrnda ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
34 32 feqmptd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑥 ) ) )
35 31 3 grpinvf ⊢ ( 𝑅 ∈ Grp → 𝑀 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
36 8 35 syl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑀 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
37 36 feqmptd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑀 = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑀 ‘ 𝑦 ) ) )
38 fveq2 ⊢ ( 𝑦 = ( 𝑋 ‘ 𝑥 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝑋 ‘ 𝑥 ) ) )
39 33 34 37 38 fmptco ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ∘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑀 ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
40 27 30 39 3eqtr4d ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝑀 ∘ 𝑋 ) )