Theorem fldextid

Description: The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	fldextid	⊢ ( 𝐹 ∈ Field → 𝐹 /FldExt 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
2	1	ressid	⊢ ( 𝐹 ∈ Field → ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) = 𝐹 )
3	2	eqcomd	⊢ ( 𝐹 ∈ Field → 𝐹 = ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) )
4		isfld	⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
5	4	simplbi	⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
6		drngring	⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
7	1	subrgid	⊢ ( 𝐹 ∈ Ring → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) )
8	5 6 7	3syl	⊢ ( 𝐹 ∈ Field → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) )
9		brfldext	⊢ ( ( 𝐹 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐹 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
10	9	anidms	⊢ ( 𝐹 ∈ Field → ( 𝐹 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
11	3 8 10	mpbir2and	⊢ ( 𝐹 ∈ Field → 𝐹 /FldExt 𝐹 )