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

Metamath Proof Explorer

Theorem fldgenid

Description: The subfield of a field F generated by the whole base set of F is F itself. (Contributed by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Hypotheses fldgenval.1 ⊢ B = Base F
fldgenval.2 ⊢ φ → F ∈ DivRing
Assertion fldgenid ⊢ φ → F fldGen B = B

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ B = Base F
2 fldgenval.2 ⊢ φ → F ∈ DivRing
3 ssidd ⊢ φ → B ⊆ B
4 1 2 3 fldgenssv ⊢ φ → F fldGen B ⊆ B
5 1 2 3 fldgenssid ⊢ φ → B ⊆ F fldGen B
6 4 5 eqssd ⊢ φ → F fldGen B = B