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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	primefldgen1.1	⊢ 1 = ( 1r ‘ 𝑅 )
	primefldgen1.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
Assertion	primefldgen1	⊢ ( 𝜑 → ∩ ( SubDRing ‘ 𝑅 ) = ( 𝑅 fldGen { 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		primefldgen1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		primefldgen1.1	⊢ 1 = ( 1r ‘ 𝑅 )
3		primefldgen1.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
4		issdrg	⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑎 ) ∈ DivRing ) )
5	4	simp2bi	⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝑅 ) → 𝑎 ∈ ( SubRing ‘ 𝑅 ) )
6	2	subrg1cl	⊢ ( 𝑎 ∈ ( SubRing ‘ 𝑅 ) → 1 ∈ 𝑎 )
7	5 6	syl	⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝑅 ) → 1 ∈ 𝑎 )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ) → 1 ∈ 𝑎 )
9	8	snssd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ) → { 1 } ⊆ 𝑎 )
10	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( SubDRing ‘ 𝑅 ) { 1 } ⊆ 𝑎 )
11		rabid2	⊢ ( ( SubDRing ‘ 𝑅 ) = { 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ∣ { 1 } ⊆ 𝑎 } ↔ ∀ 𝑎 ∈ ( SubDRing ‘ 𝑅 ) { 1 } ⊆ 𝑎 )
12	10 11	sylibr	⊢ ( 𝜑 → ( SubDRing ‘ 𝑅 ) = { 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ∣ { 1 } ⊆ 𝑎 } )
13	12	inteqd	⊢ ( 𝜑 → ∩ ( SubDRing ‘ 𝑅 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ∣ { 1 } ⊆ 𝑎 } )
14	3	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
15	1 2	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
16	14 15	syl	⊢ ( 𝜑 → 1 ∈ 𝐵 )
17	16	snssd	⊢ ( 𝜑 → { 1 } ⊆ 𝐵 )
18	1 3 17	fldgenval	⊢ ( 𝜑 → ( 𝑅 fldGen { 1 } ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑅 ) ∣ { 1 } ⊆ 𝑎 } )
19	13 18	eqtr4d	⊢ ( 𝜑 → ∩ ( SubDRing ‘ 𝑅 ) = ( 𝑅 fldGen { 1 } ) )