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	$⊢ \underset{˙}{+} = +_{N}$
	pwsmgp.q	$⊢ \underset{˙}{✚} = +_{Z}$
Assertion	pwsmgp	$⊢ (R \in V \land I \in W) \to (B = C \land \underset{˙}{+} = \underset{˙}{✚})$

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	$⊢ \underset{˙}{+} = +_{N}$
8		pwsmgp.q	$⊢ \underset{˙}{✚} = +_{Z}$
9		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
10		eqid	$⊢ {mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = {mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
11		eqid	$⊢ Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})) = Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\}))$
12		simpr	$⊢ (R \in V \land I \in W) \to I \in W$
13		fvexd	$⊢ (R \in V \land I \in W) \to Scalar (R) \in V$
14		fnconstg	$⊢ R \in V \to (I \times \{R\}) Fn I$
15	14	adantr	$⊢ (R \in V \land I \in W) \to (I \times \{R\}) Fn I$
16	9 10 11 12 13 15	prdsmgp	$⊢ (R \in V \land I \in W) \to ({Base}_{{mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}} = {Base}_{(Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})))} \land +_{{mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}} = +_{(Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})))})$
17	16	simpld	$⊢ (R \in V \land I \in W) \to {Base}_{{mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}} = {Base}_{(Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})))}$
18		eqid	$⊢ Scalar (R) = Scalar (R)$
19	1 18	pwsval	$⊢ (R \in V \land I \in W) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
20	19	fveq2d	$⊢ (R \in V \land I \in W) \to {mulGrp}_{Y} = {mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
21	4 20	eqtrid	$⊢ (R \in V \land I \in W) \to N = {mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
22	21	fveq2d	$⊢ (R \in V \land I \in W) \to {Base}_{N} = {Base}_{{mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}}$
23	2	fvexi	$⊢ M \in V$
24		eqid	$⊢ M ↑_{𝑠} I = M ↑_{𝑠} I$
25		eqid	$⊢ Scalar (M) = Scalar (M)$
26	24 25	pwsval	$⊢ (M \in V \land I \in W) \to M ↑_{𝑠} I = Scalar (M) ⨉_{𝑠} (I \times \{M\})$
27	23 12 26	sylancr	$⊢ (R \in V \land I \in W) \to M ↑_{𝑠} I = Scalar (M) ⨉_{𝑠} (I \times \{M\})$
28	2 18	mgpsca	$⊢ Scalar (R) = Scalar (M)$
29	28	eqcomi	$⊢ Scalar (M) = Scalar (R)$
30	29	a1i	$⊢ (R \in V \land I \in W) \to Scalar (M) = Scalar (R)$
31	2	sneqi	$⊢ \{M\} = \{{mulGrp}_{R}\}$
32	31	xpeq2i	$⊢ I \times \{M\} = I \times \{{mulGrp}_{R}\}$
33		fnmgp	$⊢ mulGrp Fn V$
34		elex	$⊢ R \in V \to R \in V$
35	34	adantr	$⊢ (R \in V \land I \in W) \to R \in V$
36		fcoconst	$⊢ (mulGrp Fn V \land R \in V) \to mulGrp \circ (I \times \{R\}) = I \times \{{mulGrp}_{R}\}$
37	33 35 36	sylancr	$⊢ (R \in V \land I \in W) \to mulGrp \circ (I \times \{R\}) = I \times \{{mulGrp}_{R}\}$
38	32 37	eqtr4id	$⊢ (R \in V \land I \in W) \to I \times \{M\} = mulGrp \circ (I \times \{R\})$
39	30 38	oveq12d	$⊢ (R \in V \land I \in W) \to Scalar (M) ⨉_{𝑠} (I \times \{M\}) = Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\}))$
40	27 39	eqtrd	$⊢ (R \in V \land I \in W) \to M ↑_{𝑠} I = Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\}))$
41	3 40	eqtrid	$⊢ (R \in V \land I \in W) \to Z = Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\}))$
42	41	fveq2d	$⊢ (R \in V \land I \in W) \to {Base}_{Z} = {Base}_{(Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})))}$
43	17 22 42	3eqtr4d	$⊢ (R \in V \land I \in W) \to {Base}_{N} = {Base}_{Z}$
44	43 5 6	3eqtr4g	$⊢ (R \in V \land I \in W) \to B = C$
45	16	simprd	$⊢ (R \in V \land I \in W) \to +_{{mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}} = +_{(Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})))}$
46	21	fveq2d	$⊢ (R \in V \land I \in W) \to +_{N} = +_{{mulGrp}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}}$
47	41	fveq2d	$⊢ (R \in V \land I \in W) \to +_{Z} = +_{(Scalar (R) ⨉_{𝑠} (mulGrp \circ (I \times \{R\})))}$
48	45 46 47	3eqtr4d	$⊢ (R \in V \land I \in W) \to +_{N} = +_{Z}$
49	48 7 8	3eqtr4g	$⊢ (R \in V \land I \in W) \to \underset{˙}{+} = \underset{˙}{✚}$
50	44 49	jca	$⊢ (R \in V \land I \in W) \to (B = C \land \underset{˙}{+} = \underset{˙}{✚})$

Metamath Proof Explorer

Theorem pwsmgp

Proof