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 /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ 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 → Base f = Base F
7 1 6 oveq12d ⊢ e = E ∧ f = F → e ↾ 𝑠 Base f = E ↾ 𝑠 Base F
8 3 7 eqeq12d ⊢ e = E ∧ f = F → f = e ↾ 𝑠 Base f ↔ F = E ↾ 𝑠 Base F
9 1 fveq2d ⊢ e = E ∧ f = F → SubRing ⁡ e = SubRing ⁡ E
10 6 9 eleq12d ⊢ e = E ∧ f = F → Base f ∈ SubRing ⁡ e ↔ Base F ∈ SubRing ⁡ E
11 8 10 anbi12d ⊢ e = E ∧ f = F → f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
12 5 11 anbi12d ⊢ e = E ∧ f = F → e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e ↔ E ∈ Field ∧ F ∈ Field ∧ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
13 df-fldext ⊢ /FldExt = e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e
14 12 13 brabga ⊢ E ∈ Field ∧ F ∈ Field → E /FldExt F ↔ E ∈ Field ∧ F ∈ Field ∧ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
15 14 bianabs ⊢ E ∈ Field ∧ F ∈ Field → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E