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

Metamath Proof Explorer

Theorem brfldext

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

Ref Expression
Assertion brfldext ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐸 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑒 = 𝐸 )
2 1 eleq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 ∈ Field ↔ 𝐸 ∈ Field ) )
3 simpr ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
4 3 eleq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ∈ Field ↔ 𝐹 ∈ Field ) )
5 2 4 anbi12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ↔ ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) ) )
6 3 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
7 1 6 oveq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
8 3 7 eqeq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ↔ 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) )
9 1 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( SubRing ‘ 𝑒 ) = ( SubRing ‘ 𝐸 ) )
10 6 9 eleq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ↔ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) )
11 8 10 anbi12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
12 5 11 anbi12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) ↔ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) ∧ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) ) )
13 df-fldext ⊢ /FldExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) }
14 12 13 brabga ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐸 /FldExt 𝐹 ↔ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) ∧ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) ) )
15 14 bianabs ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐸 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )