Theorem primefldgen1

Description: The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025)

	Ref	Expression
Hypotheses	primefldgen1.b	$$⊢B={\mathrm{Base}}_R$$
	primefldgen1.1	$$⊢\underset{\dot{}}{1}=1_R$$
	primefldgen1.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
Assertion	primefldgen1	Could not format assertion : No typesetting found for |- ( ph -> |^| ( SubDRing ` R ) = ( R fldGen { .1. } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		primefldgen1.b	$$⊢B={\mathrm{Base}}_R$$
2		primefldgen1.1	$$⊢\underset{\dot{}}{1}=1_R$$
3		primefldgen1.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
4		issdrg	$$⊢a\in \mathrm{SubDRing}\left(R\right)\leftrightarrow \left(R\in \mathrm{DivRing}\wedge a\in \mathrm{SubRing}\left(R\right)\wedge R{\upharpoonright }_{𝑠}a\in \mathrm{DivRing}\right)$$
5	4	simp2bi	$$⊢a\in \mathrm{SubDRing}\left(R\right)\to a\in \mathrm{SubRing}\left(R\right)$$
6	2	subrg1cl	$$⊢a\in \mathrm{SubRing}\left(R\right)\to \underset{\dot{}}{1}\in a$$
7	5 6	syl	$$⊢a\in \mathrm{SubDRing}\left(R\right)\to \underset{\dot{}}{1}\in a$$
8	7	adantl	$$⊢\left(\phi \wedge a\in \mathrm{SubDRing}\left(R\right)\right)\to \underset{\dot{}}{1}\in a$$
9	8	snssd	$$⊢\left(\phi \wedge a\in \mathrm{SubDRing}\left(R\right)\right)\to \left\{\underset{\dot{}}{1}\right\}\subseteq a$$
10	9	ralrimiva	$$⊢\phi \to \forall a\in \mathrm{SubDRing}\left(R\right)\left\{\underset{\dot{}}{1}\right\}\subseteq a$$
11		rabid2	$$⊢\mathrm{SubDRing}\left(R\right)=\left\{a\in \mathrm{SubDRing}\left(R\right)|\left\{\underset{\dot{}}{1}\right\}\subseteq a\right\}\leftrightarrow \forall a\in \mathrm{SubDRing}\left(R\right)\left\{\underset{\dot{}}{1}\right\}\subseteq a$$
12	10 11	sylibr	$$⊢\phi \to \mathrm{SubDRing}\left(R\right)=\left\{a\in \mathrm{SubDRing}\left(R\right)|\left\{\underset{\dot{}}{1}\right\}\subseteq a\right\}$$
13	12	inteqd	$$⊢\phi \to \bigcap \mathrm{SubDRing}\left(R\right)=\bigcap \left\{a\in \mathrm{SubDRing}\left(R\right)|\left\{\underset{\dot{}}{1}\right\}\subseteq a\right\}$$
14	3	drngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
15	1 2	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
16	14 15	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
17	16	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{1}\right\}\subseteq B$$
18	1 3 17	fldgenval	Could not format ( ph -> ( R fldGen { .1. } ) = |^| { a e. ( SubDRing ` R ) | { .1. } C_ a } ) : No typesetting found for |- ( ph -> ( R fldGen { .1. } ) = |^| { a e. ( SubDRing ` R ) | { .1. } C_ a } ) with typecode |-
19	13 18	eqtr4d	Could not format ( ph -> |^| ( SubDRing ` R ) = ( R fldGen { .1. } ) ) : No typesetting found for |- ( ph -> |^| ( SubDRing ` R ) = ( R fldGen { .1. } ) ) with typecode |-