This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwsmgp

Description: The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Hypotheses pwsmgp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsmgp.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
pwsmgp.z ⊢ 𝑍 = ( 𝑀 ↑s 𝐼 )
pwsmgp.n ⊢ 𝑁 = ( mulGrp ‘ 𝑌 )
pwsmgp.b ⊢ 𝐵 = ( Base ‘ 𝑁 )
pwsmgp.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
pwsmgp.p ⊢ + = ( +g ‘ 𝑁 )
pwsmgp.q ⊢ ✚ = ( +g ‘ 𝑍 )
Assertion pwsmgp ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐵 = 𝐶 ∧ + = ✚ ) )

Proof

Step Hyp Ref Expression
1 pwsmgp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsmgp.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3 pwsmgp.z ⊢ 𝑍 = ( 𝑀 ↑s 𝐼 )
4 pwsmgp.n ⊢ 𝑁 = ( mulGrp ‘ 𝑌 )
5 pwsmgp.b ⊢ 𝐵 = ( Base ‘ 𝑁 )
6 pwsmgp.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
7 pwsmgp.p ⊢ + = ( +g ‘ 𝑁 )
8 pwsmgp.q ⊢ ✚ = ( +g ‘ 𝑍 )
9 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
10 eqid ⊢ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
11 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) )
12 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ∈ 𝑊 )
13 fvexd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑅 ) ∈ V )
14 fnconstg ⊢ ( 𝑅 ∈ 𝑉 → ( 𝐼 × { 𝑅 } ) Fn 𝐼 )
15 14 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑅 } ) Fn 𝐼 )
16 9 10 11 12 13 15 prdsmgp ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( Base ‘ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) ) ∧ ( +g ‘ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) ) ) )
17 16 simpld ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) ) )
18 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
19 1 18 pwsval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
20 19 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
21 4 20 eqtrid ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑁 = ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) )
22 21 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝑁 ) = ( Base ‘ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) )
23 2 fvexi ⊢ 𝑀 ∈ V
24 eqid ⊢ ( 𝑀 ↑s 𝐼 ) = ( 𝑀 ↑s 𝐼 )
25 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
26 24 25 pwsval ⊢ ( ( 𝑀 ∈ V ∧ 𝐼 ∈ 𝑊 ) → ( 𝑀 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑀 ) Xs ( 𝐼 × { 𝑀 } ) ) )
27 23 12 26 sylancr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑀 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑀 ) Xs ( 𝐼 × { 𝑀 } ) ) )
28 2 18 mgpsca ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑀 )
29 28 eqcomi ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑅 )
30 29 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑅 ) )
31 2 sneqi ⊢ { 𝑀 } = { ( mulGrp ‘ 𝑅 ) }
32 31 xpeq2i ⊢ ( 𝐼 × { 𝑀 } ) = ( 𝐼 × { ( mulGrp ‘ 𝑅 ) } )
33 fnmgp ⊢ mulGrp Fn V
34 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
35 34 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
36 fcoconst ⊢ ( ( mulGrp Fn V ∧ 𝑅 ∈ V ) → ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { ( mulGrp ‘ 𝑅 ) } ) )
37 33 35 36 sylancr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { ( mulGrp ‘ 𝑅 ) } ) )
38 32 37 eqtr4id ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑀 } ) = ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) )
39 30 38 oveq12d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( Scalar ‘ 𝑀 ) Xs ( 𝐼 × { 𝑀 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) )
40 27 39 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑀 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) )
41 3 40 eqtrid ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑍 = ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) )
42 41 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝑍 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) ) )
43 17 22 42 3eqtr4d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝑁 ) = ( Base ‘ 𝑍 ) )
44 43 5 6 3eqtr4g ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = 𝐶 )
45 16 simprd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( +g ‘ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) ) )
46 21 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( +g ‘ 𝑁 ) = ( +g ‘ ( mulGrp ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) )
47 41 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( +g ‘ 𝑍 ) = ( +g ‘ ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) ) )
48 45 46 47 3eqtr4d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( +g ‘ 𝑁 ) = ( +g ‘ 𝑍 ) )
49 48 7 8 3eqtr4g ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → + = ✚ )
50 44 49 jca ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐵 = 𝐶 ∧ + = ✚ ) )