This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Base R
primefldgen1.1 ⊢ 1 ˙ = 1 R
primefldgen1.r ⊢ φ → R ∈ DivRing
Assertion primefldgen1 ⊢ φ → ⋂ SubDRing ⁡ R = R fldGen 1 ˙

Proof

Step Hyp Ref Expression
1 primefldgen1.b ⊢ B = Base R
2 primefldgen1.1 ⊢ 1 ˙ = 1 R
3 primefldgen1.r ⊢ φ → R ∈ DivRing
4 issdrg ⊢ a ∈ SubDRing ⁡ R ↔ R ∈ DivRing ∧ a ∈ SubRing ⁡ R ∧ R ↾ 𝑠 a ∈ DivRing
5 4 simp2bi ⊢ a ∈ SubDRing ⁡ R → a ∈ SubRing ⁡ R
6 2 subrg1cl ⊢ a ∈ SubRing ⁡ R → 1 ˙ ∈ a
7 5 6 syl ⊢ a ∈ SubDRing ⁡ R → 1 ˙ ∈ a
8 7 adantl ⊢ φ ∧ a ∈ SubDRing ⁡ R → 1 ˙ ∈ a
9 8 snssd ⊢ φ ∧ a ∈ SubDRing ⁡ R → 1 ˙ ⊆ a
10 9 ralrimiva ⊢ φ → ∀ a ∈ SubDRing ⁡ R 1 ˙ ⊆ a
11 rabid2 ⊢ SubDRing ⁡ R = a ∈ SubDRing ⁡ R | 1 ˙ ⊆ a ↔ ∀ a ∈ SubDRing ⁡ R 1 ˙ ⊆ a
12 10 11 sylibr ⊢ φ → SubDRing ⁡ R = a ∈ SubDRing ⁡ R | 1 ˙ ⊆ a
13 12 inteqd ⊢ φ → ⋂ SubDRing ⁡ R = ⋂ a ∈ SubDRing ⁡ R | 1 ˙ ⊆ a
14 3 drngringd ⊢ φ → R ∈ Ring
15 1 2 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ B
16 14 15 syl ⊢ φ → 1 ˙ ∈ B
17 16 snssd ⊢ φ → 1 ˙ ⊆ B
18 1 3 17 fldgenval ⊢ φ → R fldGen 1 ˙ = ⋂ a ∈ SubDRing ⁡ R | 1 ˙ ⊆ a
19 13 18 eqtr4d ⊢ φ → ⋂ SubDRing ⁡ R = R fldGen 1 ˙