Theorem 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={\mathrm{Base}}_G$$
	fxpsubm.c	$$⊢C={\mathrm{Base}}_W$$
	fxpsubm.f	$$⊢F=\left(x\in C⟼pAx\right)$$
	fxpsubm.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
	fxpsubrg.1	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{RingHom}W\right)$$
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={\mathrm{Base}}_G$$
2		fxpsubm.c	$$⊢C={\mathrm{Base}}_W$$
3		fxpsubm.f	$$⊢F=\left(x\in C⟼pAx\right)$$
4		fxpsubm.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
5		fxpsubrg.1	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{RingHom}W\right)$$
6		oveq1	$$⊢p=0_G\to pAx=0_{G}Ax$$
7	6	mpteq2dv	$$⊢p=0_G\to \left(x\in C⟼pAx\right)=\left(x\in C⟼0_{G}Ax\right)$$
8	3 7	eqtrid	$$⊢p=0_G\to F=\left(x\in C⟼0_{G}Ax\right)$$
9	8	eleq1d	$$⊢p=0_G\to \left(F\in \left(W\mathrm{RingHom}W\right)\leftrightarrow \left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{RingHom}W\right)\right)$$
10	5	ralrimiva	$$⊢\phi \to \forall p\in BF\in \left(W\mathrm{RingHom}W\right)$$
11		gagrp	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to G\in \mathrm{Grp}$$
12		eqid	$$⊢0_G=0_G$$
13	1 12	grpidcl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
14	4 11 13	3syl	$$⊢\phi \to 0_G\in B$$
15	9 10 14	rspcdva	$$⊢\phi \to \left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{RingHom}W\right)$$
16		rhmrcl1	$$⊢\left(x\in C⟼0_{G}Ax\right)\in \left(W\mathrm{RingHom}W\right)\to W\in \mathrm{Ring}$$
17	15 16	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
18		rhmghm	$$⊢F\in \left(W\mathrm{RingHom}W\right)\to F\in \left(W\mathrm{GrpHom}W\right)$$
19	5 18	syl	$$⊢\left(\phi \wedge p\in B\right)\to F\in \left(W\mathrm{GrpHom}W\right)$$
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 pAx=pA{1}_W$$
22		eqid	$$⊢1_W=1_W$$
23	2 22 17	ringidcld	$$⊢\phi \to 1_W\in C$$
24	23	adantr	$$⊢\left(\phi \wedge p\in B\right)\to 1_W\in C$$
25		ovexd	$$⊢\left(\phi \wedge p\in B\right)\to pA{1}_W\in \mathrm{V}$$
26	3 21 24 25	fvmptd3	$$⊢\left(\phi \wedge p\in B\right)\to F\left(1_W\right)=pA{1}_W$$
27	22 22	rhm1	$$⊢F\in \left(W\mathrm{RingHom}W\right)\to F\left(1_W\right)=1_W$$
28	5 27	syl	$$⊢\left(\phi \wedge p\in B\right)\to F\left(1_W\right)=1_W$$
29	26 28	eqtr3d	$$⊢\left(\phi \wedge p\in B\right)\to pA{1}_W=1_W$$
30	29	ralrimiva	$$⊢\phi \to \forall p\in BpA{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 \left(G\mathrm{GrpAct}C\right)\to C\in \mathrm{V}$$
35	4 34	syl	$$⊢\phi \to C\in \mathrm{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	$$⊢\left(F\in \left(W\mathrm{RingHom}W\right)\wedge z\in C\wedge y\in C\right)\to F\left(z{\cdot }_{W}y\right)=F\left(z\right){\cdot }_{W}F\left(y\right)$$
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 pAx=pA\left(z{\cdot }_{W}y\right)$$
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 pAx=pAz$$
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 pAx=pAy$$
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 |-