Theorem fxpsdrg

Description: The fixed points of a group action A on a division ring W is a sub-division-ring. Since sub-division-rings of fields are subfields (see fldsdrgfld ), ( C FixPts A ) might be called the fixed subfield under A . (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)$$
	fxpsdrg.1	$$⊢\phi \to W\in \mathrm{DivRing}$$
Assertion	fxpsdrg	Could not format assertion : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubDRing ` 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		fxpsdrg.1	$$⊢\phi \to W\in \mathrm{DivRing}$$
7	1 2 3 4 5	fxpsubrg	Could not format ( ph -> ( C FixPts A ) e. ( SubRing ` W ) ) : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubRing ` W ) ) with typecode |-
8	5	adantlr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> F e. ( W RingHom W ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> F e. ( W RingHom W ) ) with typecode |-
9	6	adantr	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> W e. DivRing ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> W e. DivRing ) with typecode |-
10	9	adantr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> W e. DivRing ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> W e. DivRing ) with typecode |-
11		gaset	$$⊢A\in \left(G\mathrm{GrpAct}C\right)\to C\in \mathrm{V}$$
12	4 11	syl	$$⊢\phi \to C\in \mathrm{V}$$
13	12 4	fxpss	Could not format ( ph -> ( C FixPts A ) C_ C ) : No typesetting found for |- ( ph -> ( C FixPts A ) C_ C ) with typecode |-
14	13	ssdifssd	Could not format ( ph -> ( ( C FixPts A ) \ { ( 0g ` W ) } ) C_ C ) : No typesetting found for |- ( ph -> ( ( C FixPts A ) \ { ( 0g ` W ) } ) C_ C ) with typecode |-
15	14	sselda	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> z e. C ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> z e. C ) with typecode |-
16	15	adantr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. C ) with typecode |-
17		eldifsni	Could not format ( z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) -> z =/= ( 0g ` W ) ) : No typesetting found for |- ( z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) -> z =/= ( 0g ` W ) ) with typecode |-
18	17	adantl	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> z =/= ( 0g ` W ) ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> z =/= ( 0g ` W ) ) with typecode |-
19	18	adantr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z =/= ( 0g ` W ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z =/= ( 0g ` W ) ) with typecode |-
20		eqid	$$⊢\mathrm{Unit}\left(W\right)=\mathrm{Unit}\left(W\right)$$
21		eqid	$$⊢0_W=0_W$$
22	2 20 21	drngunit	$$⊢W\in \mathrm{DivRing}\to \left(z\in \mathrm{Unit}\left(W\right)\leftrightarrow \left(z\in C\wedge z\ne 0_W\right)\right)$$
23	22	biimpar	$$⊢\left(W\in \mathrm{DivRing}\wedge \left(z\in C\wedge z\ne 0_W\right)\right)\to z\in \mathrm{Unit}\left(W\right)$$
24	10 16 19 23	syl12anc	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( Unit ` W ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( Unit ` W ) ) with typecode |-
25		rhmunitinv	$$⊢\left(F\in \left(W\mathrm{RingHom}W\right)\wedge z\in \mathrm{Unit}\left(W\right)\right)\to F\left({inv}_r\left(W\right)\left(z\right)\right)={inv}_r\left(W\right)\left(F\left(z\right)\right)$$
26	8 24 25	syl2anc	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` ( F ` z ) ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` ( F ` z ) ) ) with typecode |-
27		oveq2	$$⊢x={inv}_r\left(W\right)\left(z\right)\to pAx=pA{inv}_r\left(W\right)\left(z\right)$$
28		eqid	$$⊢{inv}_r\left(W\right)={inv}_r\left(W\right)$$
29	2 21 28 9 15 18	drnginvrcld	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( invr ` W ) ` z ) e. C ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( invr ` W ) ` z ) e. C ) with typecode |-
30	29	adantr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( ( invr ` W ) ` z ) e. C ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( ( invr ` W ) ` z ) e. C ) with typecode |-
31		ovexd	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A ( ( invr ` W ) ` z ) ) e. _V ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A ( ( invr ` W ) ` z ) ) e. _V ) with typecode |-
32	3 27 30 31	fvmptd3	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( p A ( ( invr ` W ) ` z ) ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` ( ( invr ` W ) ` z ) ) = ( p A ( ( invr ` W ) ` z ) ) ) with typecode |-
33		oveq2	$$⊢x=z\to pAx=pAz$$
34		ovexd	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A z ) e. _V ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A z ) e. _V ) with typecode |-
35	3 33 16 34	fvmptd3	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` z ) = ( p A z ) ) with typecode |-
36	4	adantr	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> A e. ( G GrpAct C ) ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> A e. ( G GrpAct C ) ) with typecode |-
37	36	adantr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> A e. ( G GrpAct C ) ) with typecode |-
38		simplr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) with typecode |-
39	38	eldifad	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> z e. ( C FixPts A ) ) with typecode |-
40		simpr	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> p e. B ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> p e. B ) with typecode |-
41	1 37 39 40	fxpgaeq	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A z ) = z ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A z ) = z ) with typecode |-
42	35 41	eqtrd	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` z ) = z ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( F ` z ) = z ) with typecode |-
43	42	fveq2d	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( ( invr ` W ) ` ( F ` z ) ) = ( ( invr ` W ) ` z ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( ( invr ` W ) ` ( F ` z ) ) = ( ( invr ` W ) ` z ) ) with typecode |-
44	26 32 43	3eqtr3d	Could not format ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) : No typesetting found for |- ( ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) /\ p e. B ) -> ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) with typecode |-
45	44	ralrimiva	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> A. p e. B ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> A. p e. B ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) with typecode |-
46	1 36 29	isfxp	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( ( invr ` W ) ` z ) e. ( C FixPts A ) <-> A. p e. B ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( ( invr ` W ) ` z ) e. ( C FixPts A ) <-> A. p e. B ( p A ( ( invr ` W ) ` z ) ) = ( ( invr ` W ) ` z ) ) ) with typecode |-
47	45 46	mpbird	Could not format ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) : No typesetting found for |- ( ( ph /\ z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ) -> ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) with typecode |-
48	47	ralrimiva	Could not format ( ph -> A. z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) : No typesetting found for |- ( ph -> A. z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) with typecode |-
49	28 21	issdrg2	Could not format ( ( C FixPts A ) e. ( SubDRing ` W ) <-> ( W e. DivRing /\ ( C FixPts A ) e. ( SubRing ` W ) /\ A. z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) ) : No typesetting found for |- ( ( C FixPts A ) e. ( SubDRing ` W ) <-> ( W e. DivRing /\ ( C FixPts A ) e. ( SubRing ` W ) /\ A. z e. ( ( C FixPts A ) \ { ( 0g ` W ) } ) ( ( invr ` W ) ` z ) e. ( C FixPts A ) ) ) with typecode |-
50	6 7 48 49	syl3anbrc	Could not format ( ph -> ( C FixPts A ) e. ( SubDRing ` W ) ) : No typesetting found for |- ( ph -> ( C FixPts A ) e. ( SubDRing ` W ) ) with typecode |-