Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
fxpsubm.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
fxpsubm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
fxpsubm.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
fxpsubrg.1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
fxpsdrg.1 ⊢ ( 𝜑 → 𝑊 ∈ DivRing )
Assertion fxpsdrg ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubDRing ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 fxpsubm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fxpsubm.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
3 fxpsubm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐶 ↦ ( 𝑝 𝐴 𝑥 ) )
4 fxpsubm.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
5 fxpsubrg.1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
6 fxpsdrg.1 ⊢ ( 𝜑 → 𝑊 ∈ DivRing )
7 1 2 3 4 5 fxpsubrg ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubRing ‘ 𝑊 ) )
8 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) )
9 6 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → 𝑊 ∈ DivRing )
10 9 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑊 ∈ DivRing )
11 gaset ⊢ ( 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) → 𝐶 ∈ V )
12 4 11 syl ⊢ ( 𝜑 → 𝐶 ∈ V )
13 12 4 fxpss ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ⊆ 𝐶 )
14 13 ssdifssd ⊢ ( 𝜑 → ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ 𝐶 )
15 14 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → 𝑧 ∈ 𝐶 )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 )
17 eldifsni ⊢ ( 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) → 𝑧 ≠ ( 0g ‘ 𝑊 ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → 𝑧 ≠ ( 0g ‘ 𝑊 ) )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ≠ ( 0g ‘ 𝑊 ) )
20 eqid ⊢ ( Unit ‘ 𝑊 ) = ( Unit ‘ 𝑊 )
21 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
22 2 20 21 drngunit ⊢ ( 𝑊 ∈ DivRing → ( 𝑧 ∈ ( Unit ‘ 𝑊 ) ↔ ( 𝑧 ∈ 𝐶 ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ) ) )
23 22 biimpar ⊢ ( ( 𝑊 ∈ DivRing ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑧 ≠ ( 0g ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Unit ‘ 𝑊 ) )
24 10 16 19 23 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ ( Unit ‘ 𝑊 ) )
25 rhmunitinv ⊢ ( ( 𝐹 ∈ ( 𝑊 RingHom 𝑊 ) ∧ 𝑧 ∈ ( Unit ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invr ‘ 𝑊 ) ‘ ( 𝐹 ‘ 𝑧 ) ) )
26 8 24 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invr ‘ 𝑊 ) ‘ ( 𝐹 ‘ 𝑧 ) ) )
27 oveq2 ⊢ ( 𝑥 = ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) )
28 eqid ⊢ ( invr ‘ 𝑊 ) = ( invr ‘ 𝑊 )
29 2 21 28 9 15 18 drnginvrcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ∈ 𝐶 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ∈ 𝐶 )
31 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) ∈ V )
32 3 27 30 31 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) = ( 𝑝 𝐴 ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) )
33 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 𝑧 ) )
34 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑧 ) ∈ V )
35 3 33 16 34 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑝 𝐴 𝑧 ) )
36 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
38 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
39 38 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐶 FixPts 𝐴 ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
41 1 37 39 40 fxpgaeq ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 𝑧 ) = 𝑧 )
42 35 41 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
43 42 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( ( invr ‘ 𝑊 ) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) )
44 26 32 43 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 𝐴 ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) )
45 44 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) )
46 1 36 29 isfxp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → ( ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝐵 ( 𝑝 𝐴 ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) = ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ) )
47 45 46 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) )
48 47 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) )
49 28 21 issdrg2 ⊢ ( ( 𝐶 FixPts 𝐴 ) ∈ ( SubDRing ‘ 𝑊 ) ↔ ( 𝑊 ∈ DivRing ∧ ( 𝐶 FixPts 𝐴 ) ∈ ( SubRing ‘ 𝑊 ) ∧ ∀ 𝑧 ∈ ( ( 𝐶 FixPts 𝐴 ) ∖ { ( 0g ‘ 𝑊 ) } ) ( ( invr ‘ 𝑊 ) ‘ 𝑧 ) ∈ ( 𝐶 FixPts 𝐴 ) ) )
50 6 7 48 49 syl3anbrc ⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) ∈ ( SubDRing ‘ 𝑊 ) )