fldexttr

Description: Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

		Ref	Expression
	Assertion	fldexttr	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E /_{FldExt} K$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F /_{FldExt} K$
2		simpl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E /_{FldExt} F$
3		fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$
4	2 3	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F \in Field$
5		fldextfld2	$⊢ F /_{FldExt} K \to K \in Field$
6	1 5	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to K \in Field$
7		brfldext	$⊢ (F \in Field \land K \in Field) \to (F /_{FldExt} K \leftrightarrow (K = F ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (F)))$
8	4 6 7	syl2anc	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (F /_{FldExt} K \leftrightarrow (K = F ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (F)))$
9	1 8	mpbid	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (K = F ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (F))$
10	9	simpld	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to K = F ↾_{𝑠} {Base}_{K}$
11		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
12	2 11	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E \in Field$
13		brfldext	$⊢ (E \in Field \land F \in Field) \to (E /_{FldExt} F \leftrightarrow (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E)))$
14	12 4 13	syl2anc	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (E /_{FldExt} F \leftrightarrow (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E)))$
15	2 14	mpbid	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E))$
16	15	simpld	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F = E ↾_{𝑠} {Base}_{F}$
17	16	oveq1d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F ↾_{𝑠} {Base}_{K} = (E ↾_{𝑠} {Base}_{F}) ↾_{𝑠} {Base}_{K}$
18		fvex	$⊢ {Base}_{F} \in V$
19		fvex	$⊢ {Base}_{K} \in V$
20		ressress	$⊢ ({Base}_{F} \in V \land {Base}_{K} \in V) \to (E ↾_{𝑠} {Base}_{F}) ↾_{𝑠} {Base}_{K} = E ↾_{𝑠} ({Base}_{F} \cap {Base}_{K})$
21	18 19 20	mp2an	$⊢ (E ↾_{𝑠} {Base}_{F}) ↾_{𝑠} {Base}_{K} = E ↾_{𝑠} ({Base}_{F} \cap {Base}_{K})$
22	17 21	eqtrdi	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F ↾_{𝑠} {Base}_{K} = E ↾_{𝑠} ({Base}_{F} \cap {Base}_{K})$
23		incom	$⊢ {Base}_{K} \cap {Base}_{F} = {Base}_{F} \cap {Base}_{K}$
24	9	simprd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \in SubRing (F)$
25		eqid	$⊢ {Base}_{F} = {Base}_{F}$
26	25	subrgss	$⊢ {Base}_{K} \in SubRing (F) \to {Base}_{K} \subseteq {Base}_{F}$
27	24 26	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \subseteq {Base}_{F}$
28		df-ss	$⊢ {Base}_{K} \subseteq {Base}_{F} \leftrightarrow {Base}_{K} \cap {Base}_{F} = {Base}_{K}$
29	27 28	sylib	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \cap {Base}_{F} = {Base}_{K}$
30	23 29	eqtr3id	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{F} \cap {Base}_{K} = {Base}_{K}$
31	30	oveq2d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E ↾_{𝑠} ({Base}_{F} \cap {Base}_{K}) = E ↾_{𝑠} {Base}_{K}$
32	10 22 31	3eqtrd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to K = E ↾_{𝑠} {Base}_{K}$
33	15	simprd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{F} \in SubRing (E)$
34	16	fveq2d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to SubRing (F) = SubRing (E ↾_{𝑠} {Base}_{F})$
35	24 34	eleqtrd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \in SubRing (E ↾_{𝑠} {Base}_{F})$
36		eqid	$⊢ E ↾_{𝑠} {Base}_{F} = E ↾_{𝑠} {Base}_{F}$
37	36	subsubrg	$⊢ {Base}_{F} \in SubRing (E) \to ({Base}_{K} \in SubRing (E ↾_{𝑠} {Base}_{F}) \leftrightarrow ({Base}_{K} \in SubRing (E) \land {Base}_{K} \subseteq {Base}_{F}))$
38	37	simprbda	$⊢ ({Base}_{F} \in SubRing (E) \land {Base}_{K} \in SubRing (E ↾_{𝑠} {Base}_{F})) \to {Base}_{K} \in SubRing (E)$
39	33 35 38	syl2anc	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \in SubRing (E)$
40		brfldext	$⊢ (E \in Field \land K \in Field) \to (E /_{FldExt} K \leftrightarrow (K = E ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (E)))$
41	12 6 40	syl2anc	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (E /_{FldExt} K \leftrightarrow (K = E ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (E)))$
42	32 39 41	mpbir2and	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E /_{FldExt} K$

Metamath Proof Explorer

Theorem fldexttr

Proof