Metamath Proof Explorer


Theorem fldgensdrg

Description: A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Hypotheses fldgenval.1 B = Base F
fldgenval.2 φ F DivRing
fldgenval.3 φ S B
Assertion fldgensdrg Could not format assertion : No typesetting found for |- ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 fldgenval.1 B = Base F
2 fldgenval.2 φ F DivRing
3 fldgenval.3 φ S B
4 1 2 3 fldgenval Could not format ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) : No typesetting found for |- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) with typecode |-
5 2 drngringd φ F Ring
6 eqid F 𝑠 a SubDRing F | S a = F 𝑠 a SubDRing F | S a
7 sseq2 a = x S a S x
8 7 elrab x a SubDRing F | S a x SubDRing F S x
9 8 biimpi x a SubDRing F | S a x SubDRing F S x
10 9 adantl φ x a SubDRing F | S a x SubDRing F S x
11 10 simpld φ x a SubDRing F | S a x SubDRing F
12 issdrg x SubDRing F F DivRing x SubRing F F 𝑠 x DivRing
13 12 simp2bi x SubDRing F x SubRing F
14 11 13 syl φ x a SubDRing F | S a x SubRing F
15 14 ex φ x a SubDRing F | S a x SubRing F
16 15 ssrdv φ a SubDRing F | S a SubRing F
17 sseq2 a = B S a S B
18 1 sdrgid F DivRing B SubDRing F
19 2 18 syl φ B SubDRing F
20 17 19 3 elrabd φ B a SubDRing F | S a
21 20 ne0d φ a SubDRing F | S a
22 12 simp3bi x SubDRing F F 𝑠 x DivRing
23 11 22 syl φ x a SubDRing F | S a F 𝑠 x DivRing
24 6 2 16 21 23 subdrgint φ F 𝑠 a SubDRing F | S a DivRing
25 24 drngringd φ F 𝑠 a SubDRing F | S a Ring
26 intss1 B a SubDRing F | S a a SubDRing F | S a B
27 20 26 syl φ a SubDRing F | S a B
28 issdrg a SubDRing F F DivRing a SubRing F F 𝑠 a DivRing
29 28 simp2bi a SubDRing F a SubRing F
30 eqid 1 F = 1 F
31 30 subrg1cl a SubRing F 1 F a
32 29 31 syl a SubDRing F 1 F a
33 32 ad2antlr φ a SubDRing F S a 1 F a
34 33 ex φ a SubDRing F S a 1 F a
35 34 ralrimiva φ a SubDRing F S a 1 F a
36 fvex 1 F V
37 36 elintrab 1 F a SubDRing F | S a a SubDRing F S a 1 F a
38 35 37 sylibr φ 1 F a SubDRing F | S a
39 1 30 issubrg a SubDRing F | S a SubRing F F Ring F 𝑠 a SubDRing F | S a Ring a SubDRing F | S a B 1 F a SubDRing F | S a
40 39 biimpri F Ring F 𝑠 a SubDRing F | S a Ring a SubDRing F | S a B 1 F a SubDRing F | S a a SubDRing F | S a SubRing F
41 5 25 27 38 40 syl22anc φ a SubDRing F | S a SubRing F
42 issdrg a SubDRing F | S a SubDRing F F DivRing a SubDRing F | S a SubRing F F 𝑠 a SubDRing F | S a DivRing
43 2 41 24 42 syl3anbrc φ a SubDRing F | S a SubDRing F
44 4 43 eqeltrd Could not format ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) ) : No typesetting found for |- ( ph -> ( F fldGen S ) e. ( SubDRing ` F ) ) with typecode |-