fldextrspundgdvds

Description: Given two finite extensions I / K and J / K of the same field K , the degree of the extension I / K divides the degree of the extension E / K , E being the composite field I J . (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypotheses	fldextrspun.k	$⊢ K = L ↾_{𝑠} F$
	fldextrspun.i	$⊢ I = L ↾_{𝑠} G$
	fldextrspun.j	$⊢ J = L ↾_{𝑠} H$
	fldextrspun.2	$⊢ φ \to L \in Field$
	fldextrspun.3	$⊢ φ \to F \in SubDRing (I)$
	fldextrspun.4	$⊢ φ \to F \in SubDRing (J)$
	fldextrspun.5	$⊢ φ \to G \in SubDRing (L)$
	fldextrspun.6	$⊢ φ \to H \in SubDRing (L)$
	fldextrspundglemul.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
	fldextrspundglemul.1	$⊢ E = L ↾_{𝑠} (L fldGen (G \cup H))$
	fldextrspundgledvds.1	$⊢ φ \to I [. : .] K \in ℕ$
Assertion	fldextrspundgdvds	$⊢ φ \to [I : K] ∥ [E : K]$

Proof

Step	Hyp	Ref	Expression
1		fldextrspun.k	$⊢ K = L ↾_{𝑠} F$
2		fldextrspun.i	$⊢ I = L ↾_{𝑠} G$
3		fldextrspun.j	$⊢ J = L ↾_{𝑠} H$
4		fldextrspun.2	$⊢ φ \to L \in Field$
5		fldextrspun.3	$⊢ φ \to F \in SubDRing (I)$
6		fldextrspun.4	$⊢ φ \to F \in SubDRing (J)$
7		fldextrspun.5	$⊢ φ \to G \in SubDRing (L)$
8		fldextrspun.6	$⊢ φ \to H \in SubDRing (L)$
9		fldextrspundglemul.7	$⊢ φ \to J [. : .] K \in ℕ_{0}$
10		fldextrspundglemul.1	$⊢ E = L ↾_{𝑠} (L fldGen (G \cup H))$
11		fldextrspundgledvds.1	$⊢ φ \to I [. : .] K \in ℕ$
12	1 2 3 4 5 6 7 8 9 10 11	fldextrspundgdvdslem	$⊢ φ \to E [. : .] I \in ℕ_{0}$
13	12	nn0zd	$⊢ φ \to E [. : .] I \in ℤ$
14	11	nnzd	$⊢ φ \to I [. : .] K \in ℤ$
15		eqid	$⊢ {Base}_{L} = {Base}_{L}$
16	4	flddrngd	$⊢ φ \to L \in DivRing$
17	15	sdrgss	$⊢ G \in SubDRing (L) \to G \subseteq {Base}_{L}$
18	7 17	syl	$⊢ φ \to G \subseteq {Base}_{L}$
19	15	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
20	8 19	syl	$⊢ φ \to H \subseteq {Base}_{L}$
21	18 20	unssd	$⊢ φ \to G \cup H \subseteq {Base}_{L}$
22	15 16 21	fldgensdrg	$⊢ φ \to L fldGen (G \cup H) \in SubDRing (L)$
23		eqid	$⊢ RingSpan (L) = RingSpan (L)$
24		eqid	$⊢ RingSpan (L) (G \cup H) = RingSpan (L) (G \cup H)$
25		eqid	$⊢ L ↾_{𝑠} RingSpan (L) (G \cup H) = L ↾_{𝑠} RingSpan (L) (G \cup H)$
26	1 2 3 4 5 6 7 8 9 23 24 25	fldextrspunlem2	$⊢ φ \to RingSpan (L) (G \cup H) = L fldGen (G \cup H)$
27	26	oveq2d	$⊢ φ \to L ↾_{𝑠} RingSpan (L) (G \cup H) = L ↾_{𝑠} (L fldGen (G \cup H))$
28	10 27	eqtr4id	$⊢ φ \to E = L ↾_{𝑠} RingSpan (L) (G \cup H)$
29	1 2 3 4 5 6 7 8 9 23 24 25	fldextrspunfld	$⊢ φ \to L ↾_{𝑠} RingSpan (L) (G \cup H) \in Field$
30	28 29	eqeltrd	$⊢ φ \to E \in Field$
31	30	flddrngd	$⊢ φ \to E \in DivRing$
32	31	drngringd	$⊢ φ \to E \in Ring$
33	10	oveq1i	$⊢ E ↾_{𝑠} F = (L ↾_{𝑠} (L fldGen (G \cup H))) ↾_{𝑠} F$
34		ovexd	$⊢ φ \to L fldGen (G \cup H) \in V$
35		eqid	$⊢ {Base}_{I} = {Base}_{I}$
36	35	sdrgss	$⊢ F \in SubDRing (I) \to F \subseteq {Base}_{I}$
37	5 36	syl	$⊢ φ \to F \subseteq {Base}_{I}$
38	2 15	ressbas2	$⊢ G \subseteq {Base}_{L} \to G = {Base}_{I}$
39	18 38	syl	$⊢ φ \to G = {Base}_{I}$
40	37 39	sseqtrrd	$⊢ φ \to F \subseteq G$
41		ssun1	$⊢ G \subseteq G \cup H$
42	41	a1i	$⊢ φ \to G \subseteq G \cup H$
43	40 42	sstrd	$⊢ φ \to F \subseteq G \cup H$
44	15 16 21	fldgenssid	$⊢ φ \to G \cup H \subseteq L fldGen (G \cup H)$
45	43 44	sstrd	$⊢ φ \to F \subseteq L fldGen (G \cup H)$
46		ressabs	$⊢ (L fldGen (G \cup H) \in V \land F \subseteq L fldGen (G \cup H)) \to (L ↾_{𝑠} (L fldGen (G \cup H))) ↾_{𝑠} F = L ↾_{𝑠} F$
47	34 45 46	syl2anc	$⊢ φ \to (L ↾_{𝑠} (L fldGen (G \cup H))) ↾_{𝑠} F = L ↾_{𝑠} F$
48	33 47	eqtrid	$⊢ φ \to E ↾_{𝑠} F = L ↾_{𝑠} F$
49	2	oveq1i	$⊢ I ↾_{𝑠} F = (L ↾_{𝑠} G) ↾_{𝑠} F$
50		ressabs	$⊢ (G \in SubDRing (L) \land F \subseteq G) \to (L ↾_{𝑠} G) ↾_{𝑠} F = L ↾_{𝑠} F$
51	7 40 50	syl2anc	$⊢ φ \to (L ↾_{𝑠} G) ↾_{𝑠} F = L ↾_{𝑠} F$
52	49 51	eqtrid	$⊢ φ \to I ↾_{𝑠} F = L ↾_{𝑠} F$
53	48 52	eqtr4d	$⊢ φ \to E ↾_{𝑠} F = I ↾_{𝑠} F$
54		eqid	$⊢ I ↾_{𝑠} F = I ↾_{𝑠} F$
55	54	sdrgdrng	$⊢ F \in SubDRing (I) \to I ↾_{𝑠} F \in DivRing$
56	5 55	syl	$⊢ φ \to I ↾_{𝑠} F \in DivRing$
57	53 56	eqeltrd	$⊢ φ \to E ↾_{𝑠} F \in DivRing$
58	57	drngringd	$⊢ φ \to E ↾_{𝑠} F \in Ring$
59	15 16 21	fldgenssv	$⊢ φ \to L fldGen (G \cup H) \subseteq {Base}_{L}$
60	10 15	ressbas2	$⊢ L fldGen (G \cup H) \subseteq {Base}_{L} \to L fldGen (G \cup H) = {Base}_{E}$
61	59 60	syl	$⊢ φ \to L fldGen (G \cup H) = {Base}_{E}$
62	45 61	sseqtrd	$⊢ φ \to F \subseteq {Base}_{E}$
63	16	drngringd	$⊢ φ \to L \in Ring$
64	42 44	sstrd	$⊢ φ \to G \subseteq L fldGen (G \cup H)$
65		sdrgsubrg	$⊢ G \in SubDRing (L) \to G \in SubRing (L)$
66		eqid	$⊢ 1_{L} = 1_{L}$
67	66	subrg1cl	$⊢ G \in SubRing (L) \to 1_{L} \in G$
68	7 65 67	3syl	$⊢ φ \to 1_{L} \in G$
69	64 68	sseldd	$⊢ φ \to 1_{L} \in (L fldGen (G \cup H))$
70	10 15 66	ress1r	$⊢ (L \in Ring \land 1_{L} \in (L fldGen (G \cup H)) \land L fldGen (G \cup H) \subseteq {Base}_{L}) \to 1_{L} = 1_{E}$
71	63 69 59 70	syl3anc	$⊢ φ \to 1_{L} = 1_{E}$
72	2 15 66	ress1r	$⊢ (L \in Ring \land 1_{L} \in G \land G \subseteq {Base}_{L}) \to 1_{L} = 1_{I}$
73	63 68 18 72	syl3anc	$⊢ φ \to 1_{L} = 1_{I}$
74	71 73	eqtr3d	$⊢ φ \to 1_{E} = 1_{I}$
75		sdrgsubrg	$⊢ F \in SubDRing (I) \to F \in SubRing (I)$
76		eqid	$⊢ 1_{I} = 1_{I}$
77	76	subrg1cl	$⊢ F \in SubRing (I) \to 1_{I} \in F$
78	5 75 77	3syl	$⊢ φ \to 1_{I} \in F$
79	74 78	eqeltrd	$⊢ φ \to 1_{E} \in F$
80		eqid	$⊢ {Base}_{E} = {Base}_{E}$
81		eqid	$⊢ 1_{E} = 1_{E}$
82	80 81	issubrg	$⊢ F \in SubRing (E) \leftrightarrow ((E \in Ring \land E ↾_{𝑠} F \in Ring) \land (F \subseteq {Base}_{E} \land 1_{E} \in F))$
83	32 58 62 79 82	syl22anbrc	$⊢ φ \to F \in SubRing (E)$
84		issdrg	$⊢ F \in SubDRing (E) \leftrightarrow (E \in DivRing \land F \in SubRing (E) \land E ↾_{𝑠} F \in DivRing)$
85	31 83 57 84	syl3anbrc	$⊢ φ \to F \in SubDRing (E)$
86	10 4 22 85 1	fldsdrgfldext2	$⊢ φ \to E /_{FldExt} K$
87		extdgcl	$⊢ E /_{FldExt} K \to E [. : .] K \in ℕ_{0}^{*}$
88	86 87	syl	$⊢ φ \to E [. : .] K \in ℕ_{0}^{*}$
89	11	nnnn0d	$⊢ φ \to I [. : .] K \in ℕ_{0}$
90	89 9	nn0mulcld	$⊢ φ \to [I : K] [J : K] \in ℕ_{0}$
91	1 2 3 4 5 6 7 8 9 10	fldextrspundglemul	$⊢ φ \to E [. : .] K \leq [I : K] \cdot_{𝑒} [J : K]$
92	11	nnred	$⊢ φ \to I [. : .] K \in ℝ$
93	9	nn0red	$⊢ φ \to J [. : .] K \in ℝ$
94		rexmul	$⊢ (I [. : .] K \in ℝ \land J [. : .] K \in ℝ) \to [I : K] \cdot_{𝑒} [J : K] = [I : K] [J : K]$
95	92 93 94	syl2anc	$⊢ φ \to [I : K] \cdot_{𝑒} [J : K] = [I : K] [J : K]$
96	91 95	breqtrd	$⊢ φ \to E [. : .] K \leq [I : K] [J : K]$
97		xnn0lenn0nn0	$⊢ (E [. : .] K \in ℕ_{0}^{*} \land [I : K] [J : K] \in ℕ_{0} \land E [. : .] K \leq [I : K] [J : K]) \to E [. : .] K \in ℕ_{0}$
98	88 90 96 97	syl3anc	$⊢ φ \to E [. : .] K \in ℕ_{0}$
99	98	nn0zd	$⊢ φ \to E [. : .] K \in ℤ$
100	15 2 10 4 7 20	fldgenfldext	$⊢ φ \to E /_{FldExt} I$
101	2 4 7 5 1	fldsdrgfldext2	$⊢ φ \to I /_{FldExt} K$
102		extdgmul	$⊢ (E /_{FldExt} I \land I /_{FldExt} K) \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
103	100 101 102	syl2anc	$⊢ φ \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
104	12	nn0red	$⊢ φ \to E [. : .] I \in ℝ$
105		rexmul	$⊢ (E [. : .] I \in ℝ \land I [. : .] K \in ℝ) \to [E : I] \cdot_{𝑒} [I : K] = [E : I] [I : K]$
106	104 92 105	syl2anc	$⊢ φ \to [E : I] \cdot_{𝑒} [I : K] = [E : I] [I : K]$
107	103 106	eqtr2d	$⊢ φ \to [E : I] [I : K] = E [. : .] K$
108		dvds0lem	$⊢ ((E [. : .] I \in ℤ \land I [. : .] K \in ℤ \land E [. : .] K \in ℤ) \land [E : I] [I : K] = E [. : .] K) \to [I : K] ∥ [E : K]$
109	13 14 99 107 108	syl31anc	$⊢ φ \to [I : K] ∥ [E : K]$

Metamath Proof Explorer

Theorem fldextrspundgdvds

Proof