fxpsubrg

Description: The fixed points of a group action A on a ring W is a subgring. (Contributed by Thierry Arnoux, 18-Nov-2025)

	Ref	Expression
Hypotheses	fxpsubm.b	$⊢ B = {Base}_{G}$
	fxpsubm.c	$⊢ C = {Base}_{W}$
	fxpsubm.f	$⊢ F = (x \in C ⟼ p A x)$
	fxpsubm.a	$⊢ φ \to A \in (G GrpAct C)$
	fxpsubrg.1	$⊢ (φ \land p \in B) \to F \in (W RingHom W)$
Assertion	fxpsubrg	Could not format assertion : No typesetting found for \|- ( ph -> ( C FixPts A ) e. ( SubRing ` W ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		fxpsubm.b	$⊢ B = {Base}_{G}$
2		fxpsubm.c	$⊢ C = {Base}_{W}$
3		fxpsubm.f	$⊢ F = (x \in C ⟼ p A x)$
4		fxpsubm.a	$⊢ φ \to A \in (G GrpAct C)$
5		fxpsubrg.1	$⊢ (φ \land p \in B) \to F \in (W RingHom W)$
6		oveq1	$⊢ p = 0_{G} \to p A x = 0_{G} A x$
7	6	mpteq2dv	$⊢ p = 0_{G} \to (x \in C ⟼ p A x) = (x \in C ⟼ 0_{G} A x)$
8	3 7	eqtrid	$⊢ p = 0_{G} \to F = (x \in C ⟼ 0_{G} A x)$
9	8	eleq1d	$⊢ p = 0_{G} \to (F \in (W RingHom W) \leftrightarrow (x \in C ⟼ 0_{G} A x) \in (W RingHom W))$
10	5	ralrimiva	$⊢ φ \to \forall p \in B F \in (W RingHom W)$
11		gagrp	$⊢ A \in (G GrpAct C) \to G \in Grp$
12		eqid	$⊢ 0_{G} = 0_{G}$
13	1 12	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
14	4 11 13	3syl	$⊢ φ \to 0_{G} \in B$
15	9 10 14	rspcdva	$⊢ φ \to (x \in C ⟼ 0_{G} A x) \in (W RingHom W)$
16		rhmrcl1	$⊢ (x \in C ⟼ 0_{G} A x) \in (W RingHom W) \to W \in Ring$
17	15 16	syl	$⊢ φ \to W \in Ring$
18		rhmghm	$⊢ F \in (W RingHom W) \to F \in (W GrpHom W)$
19	5 18	syl	$⊢ (φ \land p \in B) \to F \in (W GrpHom W)$
20	1 2 3 4 19	fxpsubg	Could not format ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) ) : No typesetting found for \|- ( ph -> ( C FixPts A ) e. ( SubGrp ` W ) ) with typecode \|-
21		oveq2	$⊢ x = 1_{W} \to p A x = p A 1_{W}$
22		eqid	$⊢ 1_{W} = 1_{W}$
23	2 22 17	ringidcld	$⊢ φ \to 1_{W} \in C$
24	23	adantr	$⊢ (φ \land p \in B) \to 1_{W} \in C$
25		ovexd	$⊢ (φ \land p \in B) \to p A 1_{W} \in V$
26	3 21 24 25	fvmptd3	$⊢ (φ \land p \in B) \to F (1_{W}) = p A 1_{W}$
27	22 22	rhm1	$⊢ F \in (W RingHom W) \to F (1_{W}) = 1_{W}$
28	5 27	syl	$⊢ (φ \land p \in B) \to F (1_{W}) = 1_{W}$
29	26 28	eqtr3d	$⊢ (φ \land p \in B) \to p A 1_{W} = 1_{W}$
30	29	ralrimiva	$⊢ φ \to \forall p \in B p A 1_{W} = 1_{W}$
31	1 4 23	isfxp	Could not format ( ph -> ( ( 1r ` W ) e. ( C FixPts A ) <-> A. p e. B ( p A ( 1r ` W ) ) = ( 1r ` W ) ) ) : No typesetting found for \|- ( ph -> ( ( 1r ` W ) e. ( C FixPts A ) <-> A. p e. B ( p A ( 1r ` W ) ) = ( 1r ` W ) ) ) with typecode \|-
32	30 31	mpbird	Could not format ( ph -> ( 1r ` W ) e. ( C FixPts A ) ) : No typesetting found for \|- ( ph -> ( 1r ` W ) e. ( C FixPts A ) ) with typecode \|-
33	5	ad4ant14	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W RingHom W ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> F e. ( W RingHom W ) ) with typecode \|-
34		gaset	$⊢ A \in (G GrpAct C) \to C \in V$
35	4 34	syl	$⊢ φ \to C \in V$
36	35 4	fxpss	Could not format ( ph -> ( C FixPts A ) C_ C ) : No typesetting found for \|- ( ph -> ( C FixPts A ) C_ C ) with typecode \|-
37	36	sselda	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> z e. C ) : No typesetting found for \|- ( ( ph /\ z e. ( C FixPts A ) ) -> z e. C ) with typecode \|-
38	37	adantr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. C ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> z e. C ) with typecode \|-
39	38	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. C ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. C ) with typecode \|-
40	36	adantr	Could not format ( ( ph /\ z e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C ) : No typesetting found for \|- ( ( ph /\ z e. ( C FixPts A ) ) -> ( C FixPts A ) C_ C ) with typecode \|-
41	40	sselda	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> y e. C ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> y e. C ) with typecode \|-
42	41	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. C ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. C ) with typecode \|-
43		eqid	$⊢ \cdot_{W} = \cdot_{W}$
44	2 43 43	rhmmul	$⊢ (F \in (W RingHom W) \land z \in C \land y \in C) \to F (z \cdot_{W} y) = F (z) \cdot_{W} F (y)$
45	33 39 42 44	syl3anc	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( .r ` W ) y ) ) = ( ( F ` z ) ( .r ` W ) ( F ` y ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( .r ` W ) y ) ) = ( ( F ` z ) ( .r ` W ) ( F ` y ) ) ) with typecode \|-
46		oveq2	$⊢ x = z \cdot_{W} y \to p A x = p A (z \cdot_{W} y)$
47	17	ad2antrr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> W e. Ring ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> W e. Ring ) with typecode \|-
48	2 43 47 38 41	ringcld	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( .r ` W ) y ) e. C ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( .r ` W ) y ) e. C ) with typecode \|-
49		ovexd	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( p A ( z ( .r ` W ) y ) ) e. _V ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( p A ( z ( .r ` W ) y ) ) e. _V ) with typecode \|-
50	3 46 48 49	fvmptd3	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( F ` ( z ( .r ` W ) y ) ) = ( p A ( z ( .r ` W ) y ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( F ` ( z ( .r ` W ) y ) ) = ( p A ( z ( .r ` W ) y ) ) ) with typecode \|-
51	50	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( .r ` W ) y ) ) = ( p A ( z ( .r ` W ) y ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` ( z ( .r ` W ) y ) ) = ( p A ( z ( .r ` W ) y ) ) ) with typecode \|-
52		oveq2	$⊢ x = z \to p A x = p A z$
53		ovexd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) e. _V ) with typecode \|-
54	3 52 39 53	fvmptd3	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) with typecode \|-
55	4	ad2antrr	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A e. ( G GrpAct C ) ) with typecode \|-
56	55	adantr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) with typecode \|-
57		simpllr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) with typecode \|-
58		simpr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> p e. B ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> p e. B ) with typecode \|-
59	1 56 57 58	fxpgaeq	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A z ) = z ) with typecode \|-
60	54 59	eqtrd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` z ) = z ) with typecode \|-
61		oveq2	$⊢ x = y \to p A x = p A y$
62		ovexd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) e. _V ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) e. _V ) with typecode \|-
63	3 61 42 62	fvmptd3	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = ( p A y ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = ( p A y ) ) with typecode \|-
64		simplr	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. ( C FixPts A ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> y e. ( C FixPts A ) ) with typecode \|-
65	1 56 64 58	fxpgaeq	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) = y ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A y ) = y ) with typecode \|-
66	63 65	eqtrd	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = y ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( F ` y ) = y ) with typecode \|-
67	60 66	oveq12d	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( ( F ` z ) ( .r ` W ) ( F ` y ) ) = ( z ( .r ` W ) y ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( ( F ` z ) ( .r ` W ) ( F ` y ) ) = ( z ( .r ` W ) y ) ) with typecode \|-
68	45 51 67	3eqtr3d	Could not format ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) : No typesetting found for \|- ( ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) /\ p e. B ) -> ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) with typecode \|-
69	68	ralrimiva	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A. p e. B ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> A. p e. B ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) with typecode \|-
70	1 55 48	isfxp	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( ( z ( .r ` W ) y ) e. ( C FixPts A ) <-> A. p e. B ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( ( z ( .r ` W ) y ) e. ( C FixPts A ) <-> A. p e. B ( p A ( z ( .r ` W ) y ) ) = ( z ( .r ` W ) y ) ) ) with typecode \|-
71	69 70	mpbird	Could not format ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( .r ` W ) y ) e. ( C FixPts A ) ) : No typesetting found for \|- ( ( ( ph /\ z e. ( C FixPts A ) ) /\ y e. ( C FixPts A ) ) -> ( z ( .r ` W ) y ) e. ( C FixPts A ) ) with typecode \|-
72	71	anasss	Could not format ( ( ph /\ ( z e. ( C FixPts A ) /\ y e. ( C FixPts A ) ) ) -> ( z ( .r ` W ) y ) e. ( C FixPts A ) ) : No typesetting found for \|- ( ( ph /\ ( z e. ( C FixPts A ) /\ y e. ( C FixPts A ) ) ) -> ( z ( .r ` W ) y ) e. ( C FixPts A ) ) with typecode \|-
73	72	ralrimivva	Could not format ( ph -> A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) : No typesetting found for \|- ( ph -> A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) with typecode \|-
74	2 22 43	issubrg2	Could not format ( W e. Ring -> ( ( C FixPts A ) e. ( SubRing ` W ) <-> ( ( C FixPts A ) e. ( SubGrp ` W ) /\ ( 1r ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) ) ) : No typesetting found for \|- ( W e. Ring -> ( ( C FixPts A ) e. ( SubRing ` W ) <-> ( ( C FixPts A ) e. ( SubGrp ` W ) /\ ( 1r ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) ) ) with typecode \|-
75	74	biimpar	Could not format ( ( W e. Ring /\ ( ( C FixPts A ) e. ( SubGrp ` W ) /\ ( 1r ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) ) -> ( C FixPts A ) e. ( SubRing ` W ) ) : No typesetting found for \|- ( ( W e. Ring /\ ( ( C FixPts A ) e. ( SubGrp ` W ) /\ ( 1r ` W ) e. ( C FixPts A ) /\ A. z e. ( C FixPts A ) A. y e. ( C FixPts A ) ( z ( .r ` W ) y ) e. ( C FixPts A ) ) ) -> ( C FixPts A ) e. ( SubRing ` W ) ) with typecode \|-
76	17 20 32 73 75	syl13anc	Could not format ( ph -> ( C FixPts A ) e. ( SubRing ` W ) ) : No typesetting found for \|- ( ph -> ( C FixPts A ) e. ( SubRing ` W ) ) with typecode \|-

Metamath Proof Explorer

Theorem fxpsubrg

Proof