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	syl5eq	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑁 = ( 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		fnmgp	⊢ mulGrp Fn V
32		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
33	32	adantr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
34		fcoconst	⊢ ( ( mulGrp Fn V ∧ 𝑅 ∈ V ) → ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { ( mulGrp ‘ 𝑅 ) } ) )
35	31 33 34	sylancr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) = ( 𝐼 × { ( mulGrp ‘ 𝑅 ) } ) )
36	2	sneqi	⊢ { 𝑀 } = { ( mulGrp ‘ 𝑅 ) }
37	36	xpeq2i	⊢ ( 𝐼 × { 𝑀 } ) = ( 𝐼 × { ( mulGrp ‘ 𝑅 ) } )
38	35 37	syl6reqr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑀 } ) = ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) )
39	30 38	oveq12d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( Scalar ‘ 𝑀 ) Xs ( 𝐼 × { 𝑀 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) )
40	27 39	eqtrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑀 ↑s 𝐼 ) = ( ( Scalar ‘ 𝑅 ) Xs ( mulGrp ∘ ( 𝐼 × { 𝑅 } ) ) ) )
41	3 40	syl5eq	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑍 = ( ( 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	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐵 = 𝐶 ∧ + = ✚ ) )