Metamath Proof Explorer

Theorem brfldext

Description: The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion brfldext ⊢E∈Field∧F∈Field→E/FldExtF↔F=E↾𝑠BaseF∧BaseF∈SubRing⁡E

Proof

Step Hyp Ref Expression
1 simpl ⊢e=E∧f=F→e=E
2 1 eleq1d ⊢e=E∧f=F→e∈Field↔E∈Field
3 simpr ⊢e=E∧f=F→f=F
4 3 eleq1d ⊢e=E∧f=F→f∈Field↔F∈Field
5 2 4 anbi12d ⊢e=E∧f=F→e∈Field∧f∈Field↔E∈Field∧F∈Field
6 3 fveq2d ⊢e=E∧f=F→Basef=BaseF
7 1 6 oveq12d ⊢e=E∧f=F→e↾𝑠Basef=E↾𝑠BaseF
8 3 7 eqeq12d ⊢e=E∧f=F→f=e↾𝑠Basef↔F=E↾𝑠BaseF
9 1 fveq2d ⊢e=E∧f=F→SubRing⁡e=SubRing⁡E
10 6 9 eleq12d ⊢e=E∧f=F→Basef∈SubRing⁡e↔BaseF∈SubRing⁡E
11 8 10 anbi12d ⊢e=E∧f=F→f=e↾𝑠Basef∧Basef∈SubRing⁡e↔F=E↾𝑠BaseF∧BaseF∈SubRing⁡E
12 5 11 anbi12d ⊢e=E∧f=F→e∈Field∧f∈Field∧f=e↾𝑠Basef∧Basef∈SubRing⁡e↔E∈Field∧F∈Field∧F=E↾𝑠BaseF∧BaseF∈SubRing⁡E
13 df-fldext ⊢/FldExt=ef|e∈Field∧f∈Field∧f=e↾𝑠Basef∧Basef∈SubRing⁡e
14 12 13 brabga ⊢E∈Field∧F∈Field→E/FldExtF↔E∈Field∧F∈Field∧F=E↾𝑠BaseF∧BaseF∈SubRing⁡E
15 14 bianabs ⊢E∈Field∧F∈Field→E/FldExtF↔F=E↾𝑠BaseF∧BaseF∈SubRing⁡E