mgpress

Description: Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof shortened by AV, 18-Oct-2024)

	Ref	Expression
Hypotheses	mgpress.1	$⊢ S = R ↾_{𝑠} A$
	mgpress.2	$⊢ M = {mulGrp}_{R}$
Assertion	mgpress	$⊢ (R \in V \land A \in W) \to M ↾_{𝑠} A = {mulGrp}_{S}$

Proof

Step	Hyp	Ref	Expression
1		mgpress.1	$⊢ S = R ↾_{𝑠} A$
2		mgpress.2	$⊢ M = {mulGrp}_{R}$
3		simpr	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to {Base}_{R} \subseteq A$
4	2	fvexi	$⊢ M \in V$
5	4	a1i	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to M \in V$
6		simplr	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to A \in W$
7		eqid	$⊢ M ↾_{𝑠} A = M ↾_{𝑠} A$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	2 8	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
10	7 9	ressid2	$⊢ ({Base}_{R} \subseteq A \land M \in V \land A \in W) \to M ↾_{𝑠} A = M$
11	3 5 6 10	syl3anc	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to M ↾_{𝑠} A = M$
12		simpll	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to R \in V$
13	1 8	ressid2	$⊢ ({Base}_{R} \subseteq A \land R \in V \land A \in W) \to S = R$
14	3 12 6 13	syl3anc	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to S = R$
15	14	fveq2d	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to {mulGrp}_{S} = {mulGrp}_{R}$
16	2 11 15	3eqtr4a	$⊢ ((R \in V \land A \in W) \land {Base}_{R} \subseteq A) \to M ↾_{𝑠} A = {mulGrp}_{S}$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18	2 17	mgpval	$⊢ M = R sSet ⟨+_{ndx}, \cdot_{R}⟩$
19	18	oveq1i	$⊢ M sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩ = (R sSet ⟨+_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩$
20		simpr	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to \neg {Base}_{R} \subseteq A$
21	4	a1i	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to M \in V$
22		simplr	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to A \in W$
23	7 9	ressval2	$⊢ (\neg {Base}_{R} \subseteq A \land M \in V \land A \in W) \to M ↾_{𝑠} A = M sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩$
24	20 21 22 23	syl3anc	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to M ↾_{𝑠} A = M sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩$
25		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
26		eqid	$⊢ \cdot_{S} = \cdot_{S}$
27	25 26	mgpval	$⊢ {mulGrp}_{S} = S sSet ⟨+_{ndx}, \cdot_{S}⟩$
28		simpll	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to R \in V$
29	1 8	ressval2	$⊢ (\neg {Base}_{R} \subseteq A \land R \in V \land A \in W) \to S = R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩$
30	20 28 22 29	syl3anc	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to S = R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩$
31	1 17	ressmulr	$⊢ A \in W \to \cdot_{R} = \cdot_{S}$
32	31	eqcomd	$⊢ A \in W \to \cdot_{S} = \cdot_{R}$
33	32	ad2antlr	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to \cdot_{S} = \cdot_{R}$
34	33	opeq2d	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to ⟨+_{ndx}, \cdot_{S}⟩ = ⟨+_{ndx}, \cdot_{R}⟩$
35	30 34	oveq12d	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to S sSet ⟨+_{ndx}, \cdot_{S}⟩ = (R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩) sSet ⟨+_{ndx}, \cdot_{R}⟩$
36	27 35	eqtrid	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to {mulGrp}_{S} = (R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩) sSet ⟨+_{ndx}, \cdot_{R}⟩$
37		basendxnplusgndx	$⊢ {Base}_{ndx} \neq +_{ndx}$
38	37	necomi	$⊢ +_{ndx} \neq {Base}_{ndx}$
39		fvex	$⊢ \cdot_{R} \in V$
40		fvex	$⊢ {Base}_{R} \in V$
41	40	inex2	$⊢ A \cap {Base}_{R} \in V$
42		fvex	$⊢ +_{ndx} \in V$
43		fvex	$⊢ {Base}_{ndx} \in V$
44	42 43	setscom	$⊢ ((R \in V \land +_{ndx} \neq {Base}_{ndx}) \land (\cdot_{R} \in V \land A \cap {Base}_{R} \in V)) \to (R sSet ⟨+_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩ = (R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩) sSet ⟨+_{ndx}, \cdot_{R}⟩$
45	39 41 44	mpanr12	$⊢ (R \in V \land +_{ndx} \neq {Base}_{ndx}) \to (R sSet ⟨+_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩ = (R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩) sSet ⟨+_{ndx}, \cdot_{R}⟩$
46	28 38 45	sylancl	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to (R sSet ⟨+_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩ = (R sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩) sSet ⟨+_{ndx}, \cdot_{R}⟩$
47	36 46	eqtr4d	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to {mulGrp}_{S} = (R sSet ⟨+_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, A \cap {Base}_{R}⟩$
48	19 24 47	3eqtr4a	$⊢ ((R \in V \land A \in W) \land \neg {Base}_{R} \subseteq A) \to M ↾_{𝑠} A = {mulGrp}_{S}$
49	16 48	pm2.61dan	$⊢ (R \in V \land A \in W) \to M ↾_{𝑠} A = {mulGrp}_{S}$

Metamath Proof Explorer

Theorem mgpress

Proof