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 ‘ 𝐸 ) ) ) )