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 ⊢ Y = R ↑ 𝑠 I
pwsmgp.m ⊢ M = mulGrp R
pwsmgp.z ⊢ Z = M ↑ 𝑠 I
pwsmgp.n ⊢ N = mulGrp Y
pwsmgp.b ⊢ B = Base N
pwsmgp.c ⊢ C = Base Z
pwsmgp.p ⊢ + ˙ = + N
pwsmgp.q ⊢ ✚ ˙ = + Z
Assertion pwsmgp ⊢ R ∈ V ∧ I ∈ W → B = C ∧ + ˙ = ✚ ˙

Proof

Step Hyp Ref Expression
1 pwsmgp.y ⊢ Y = R ↑ 𝑠 I
2 pwsmgp.m ⊢ M = mulGrp R
3 pwsmgp.z ⊢ Z = M ↑ 𝑠 I
4 pwsmgp.n ⊢ N = mulGrp Y
5 pwsmgp.b ⊢ B = Base N
6 pwsmgp.c ⊢ C = Base Z
7 pwsmgp.p ⊢ + ˙ = + N
8 pwsmgp.q ⊢ ✚ ˙ = + Z
9 eqid ⊢ Scalar ⁡ R ⨉ 𝑠 I × R = Scalar ⁡ R ⨉ 𝑠 I × R
10 eqid ⊢ mulGrp Scalar ⁡ R ⨉ 𝑠 I × R = mulGrp Scalar ⁡ R ⨉ 𝑠 I × R
11 eqid ⊢ Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R = Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
12 simpr ⊢ R ∈ V ∧ I ∈ W → I ∈ W
13 fvexd ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ R ∈ V
14 fnconstg ⊢ R ∈ V → I × R Fn I
15 14 adantr ⊢ R ∈ V ∧ I ∈ W → I × R Fn I
16 9 10 11 12 13 15 prdsmgp ⊢ R ∈ V ∧ I ∈ W → Base mulGrp Scalar ⁡ R ⨉ 𝑠 I × R = Base Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R ∧ + mulGrp Scalar ⁡ R ⨉ 𝑠 I × R = + Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
17 16 simpld ⊢ R ∈ V ∧ I ∈ W → Base mulGrp Scalar ⁡ R ⨉ 𝑠 I × R = Base Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
18 eqid ⊢ Scalar ⁡ R = Scalar ⁡ R
19 1 18 pwsval ⊢ R ∈ V ∧ I ∈ W → Y = Scalar ⁡ R ⨉ 𝑠 I × R
20 19 fveq2d ⊢ R ∈ V ∧ I ∈ W → mulGrp Y = mulGrp Scalar ⁡ R ⨉ 𝑠 I × R
21 4 20 eqtrid ⊢ R ∈ V ∧ I ∈ W → N = mulGrp Scalar ⁡ R ⨉ 𝑠 I × R
22 21 fveq2d ⊢ R ∈ V ∧ I ∈ W → Base N = Base mulGrp Scalar ⁡ R ⨉ 𝑠 I × R
23 2 fvexi ⊢ M ∈ V
24 eqid ⊢ M ↑ 𝑠 I = M ↑ 𝑠 I
25 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
26 24 25 pwsval ⊢ M ∈ V ∧ I ∈ W → M ↑ 𝑠 I = Scalar ⁡ M ⨉ 𝑠 I × M
27 23 12 26 sylancr ⊢ R ∈ V ∧ I ∈ W → M ↑ 𝑠 I = Scalar ⁡ M ⨉ 𝑠 I × M
28 2 18 mgpsca ⊢ Scalar ⁡ R = Scalar ⁡ M
29 28 eqcomi ⊢ Scalar ⁡ M = Scalar ⁡ R
30 29 a1i ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ M = Scalar ⁡ R
31 2 sneqi ⊢ M = mulGrp R
32 31 xpeq2i ⊢ I × M = I × mulGrp R
33 fnmgp ⊢ mulGrp Fn V
34 elex ⊢ R ∈ V → R ∈ V
35 34 adantr ⊢ R ∈ V ∧ I ∈ W → R ∈ V
36 fcoconst ⊢ mulGrp Fn V ∧ R ∈ V → mulGrp ∘ I × R = I × mulGrp R
37 33 35 36 sylancr ⊢ R ∈ V ∧ I ∈ W → mulGrp ∘ I × R = I × mulGrp R
38 32 37 eqtr4id ⊢ R ∈ V ∧ I ∈ W → I × M = mulGrp ∘ I × R
39 30 38 oveq12d ⊢ R ∈ V ∧ I ∈ W → Scalar ⁡ M ⨉ 𝑠 I × M = Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
40 27 39 eqtrd ⊢ R ∈ V ∧ I ∈ W → M ↑ 𝑠 I = Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
41 3 40 eqtrid ⊢ R ∈ V ∧ I ∈ W → Z = Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
42 41 fveq2d ⊢ R ∈ V ∧ I ∈ W → Base Z = Base Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
43 17 22 42 3eqtr4d ⊢ R ∈ V ∧ I ∈ W → Base N = Base Z
44 43 5 6 3eqtr4g ⊢ R ∈ V ∧ I ∈ W → B = C
45 16 simprd ⊢ R ∈ V ∧ I ∈ W → + mulGrp Scalar ⁡ R ⨉ 𝑠 I × R = + Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
46 21 fveq2d ⊢ R ∈ V ∧ I ∈ W → + N = + mulGrp Scalar ⁡ R ⨉ 𝑠 I × R
47 41 fveq2d ⊢ R ∈ V ∧ I ∈ W → + Z = + Scalar ⁡ R ⨉ 𝑠 mulGrp ∘ I × R
48 45 46 47 3eqtr4d ⊢ R ∈ V ∧ I ∈ W → + N = + Z
49 48 7 8 3eqtr4g ⊢ R ∈ V ∧ I ∈ W → + ˙ = ✚ ˙
50 44 49 jca ⊢ R ∈ V ∧ I ∈ W → B = C ∧ + ˙ = ✚ ˙