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 = {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)$
	fxpsdrg.1	$⊢ φ \to W \in 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 = {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		fxpsdrg.1	$⊢ φ \to W \in 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 (G GrpAct C) \to C \in V$
12	4 11	syl	$⊢ φ \to C \in 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	$⊢ Unit (W) = Unit (W)$
21		eqid	$⊢ 0_{W} = 0_{W}$
22	2 20 21	drngunit	$⊢ W \in DivRing \to (z \in Unit (W) \leftrightarrow (z \in C \land z \neq 0_{W}))$
23	22	biimpar	$⊢ (W \in DivRing \land (z \in C \land z \neq 0_{W})) \to z \in Unit (W)$
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	$⊢ (F \in (W RingHom W) \land z \in Unit (W)) \to F ({inv}_{r} (W) (z)) = {inv}_{r} (W) (F (z))$
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} (W) (z) \to p A x = p A {inv}_{r} (W) (z)$
28		eqid	$⊢ {inv}_{r} (W) = {inv}_{r} (W)$
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 p A x = p A z$
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 \|-

Metamath Proof Explorer

Theorem fxpsdrg

Proof