fldextrspundgdvdslem

	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	fldextrspundgdvdslem	$⊢ φ \to E [. : .] I \in ℕ_{0}$

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		eqid	$⊢ {Base}_{L} = {Base}_{L}$
13	12	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
14	8 13	syl	$⊢ φ \to H \subseteq {Base}_{L}$
15	12 2 10 4 7 14	fldgenfldext	$⊢ φ \to E /_{FldExt} I$
16		extdgcl	$⊢ E /_{FldExt} I \to E [. : .] I \in ℕ_{0}^{*}$
17	15 16	syl	$⊢ φ \to E [. : .] I \in ℕ_{0}^{*}$
18		elxnn0	$⊢ E [. : .] I \in ℕ_{0}^{*} \leftrightarrow (E [. : .] I \in ℕ_{0} \lor E [. : .] I = +∞)$
19	17 18	sylib	$⊢ φ \to (E [. : .] I \in ℕ_{0} \lor E [. : .] I = +∞)$
20	2 4 7 5 1	fldsdrgfldext2	$⊢ φ \to I /_{FldExt} K$
21		extdgmul	$⊢ (E /_{FldExt} I \land I /_{FldExt} K) \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
22	15 20 21	syl2anc	$⊢ φ \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
23	22	adantr	$⊢ (φ \land E [. : .] I = +∞) \to E [. : .] K = [E : I] \cdot_{𝑒} [I : K]$
24		simpr	$⊢ (φ \land E [. : .] I = +∞) \to E [. : .] I = +∞$
25	24	oveq1d	$⊢ (φ \land E [. : .] I = +∞) \to [E : I] \cdot_{𝑒} [I : K] = +∞ \cdot_{𝑒} [I : K]$
26	11	nnred	$⊢ φ \to I [. : .] K \in ℝ$
27	26	rexrd	$⊢ φ \to I [. : .] K \in ℝ^{*}$
28	27	adantr	$⊢ (φ \land E [. : .] I = +∞) \to I [. : .] K \in ℝ^{*}$
29	11	nngt0d	$⊢ φ \to 0 < I [. : .] K$
30	29	adantr	$⊢ (φ \land E [. : .] I = +∞) \to 0 < I [. : .] K$
31		xmulpnf2	$⊢ (I [. : .] K \in ℝ^{*} \land 0 < I [. : .] K) \to +∞ \cdot_{𝑒} [I : K] = +∞$
32	28 30 31	syl2anc	$⊢ (φ \land E [. : .] I = +∞) \to +∞ \cdot_{𝑒} [I : K] = +∞$
33	23 25 32	3eqtrd	$⊢ (φ \land E [. : .] I = +∞) \to E [. : .] K = +∞$
34	4	flddrngd	$⊢ φ \to L \in DivRing$
35	12	sdrgss	$⊢ G \in SubDRing (L) \to G \subseteq {Base}_{L}$
36	7 35	syl	$⊢ φ \to G \subseteq {Base}_{L}$
37	36 14	unssd	$⊢ φ \to G \cup H \subseteq {Base}_{L}$
38	12 34 37	fldgensdrg	$⊢ φ \to L fldGen (G \cup H) \in SubDRing (L)$
39		eqid	$⊢ RingSpan (L) = RingSpan (L)$
40		eqid	$⊢ RingSpan (L) (G \cup H) = RingSpan (L) (G \cup H)$
41		eqid	$⊢ L ↾_{𝑠} RingSpan (L) (G \cup H) = L ↾_{𝑠} RingSpan (L) (G \cup H)$
42	1 2 3 4 5 6 7 8 9 39 40 41	fldextrspunlem2	$⊢ φ \to RingSpan (L) (G \cup H) = L fldGen (G \cup H)$
43	42	oveq2d	$⊢ φ \to L ↾_{𝑠} RingSpan (L) (G \cup H) = L ↾_{𝑠} (L fldGen (G \cup H))$
44	10 43	eqtr4id	$⊢ φ \to E = L ↾_{𝑠} RingSpan (L) (G \cup H)$
45	1 2 3 4 5 6 7 8 9 39 40 41	fldextrspunfld	$⊢ φ \to L ↾_{𝑠} RingSpan (L) (G \cup H) \in Field$
46	44 45	eqeltrd	$⊢ φ \to E \in Field$
47	46	flddrngd	$⊢ φ \to E \in DivRing$
48	47	drngringd	$⊢ φ \to E \in Ring$
49	10	oveq1i	$⊢ E ↾_{𝑠} F = (L ↾_{𝑠} (L fldGen (G \cup H))) ↾_{𝑠} F$
50		ovexd	$⊢ φ \to L fldGen (G \cup H) \in V$
51		eqid	$⊢ {Base}_{I} = {Base}_{I}$
52	51	sdrgss	$⊢ F \in SubDRing (I) \to F \subseteq {Base}_{I}$
53	5 52	syl	$⊢ φ \to F \subseteq {Base}_{I}$
54	2 12	ressbas2	$⊢ G \subseteq {Base}_{L} \to G = {Base}_{I}$
55	36 54	syl	$⊢ φ \to G = {Base}_{I}$
56	53 55	sseqtrrd	$⊢ φ \to F \subseteq G$
57		ssun1	$⊢ G \subseteq G \cup H$
58	57	a1i	$⊢ φ \to G \subseteq G \cup H$
59	56 58	sstrd	$⊢ φ \to F \subseteq G \cup H$
60	12 34 37	fldgenssid	$⊢ φ \to G \cup H \subseteq L fldGen (G \cup H)$
61	59 60	sstrd	$⊢ φ \to F \subseteq L fldGen (G \cup H)$
62		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$
63	50 61 62	syl2anc	$⊢ φ \to (L ↾_{𝑠} (L fldGen (G \cup H))) ↾_{𝑠} F = L ↾_{𝑠} F$
64	49 63	eqtrid	$⊢ φ \to E ↾_{𝑠} F = L ↾_{𝑠} F$
65	2	oveq1i	$⊢ I ↾_{𝑠} F = (L ↾_{𝑠} G) ↾_{𝑠} F$
66		ressabs	$⊢ (G \in SubDRing (L) \land F \subseteq G) \to (L ↾_{𝑠} G) ↾_{𝑠} F = L ↾_{𝑠} F$
67	7 56 66	syl2anc	$⊢ φ \to (L ↾_{𝑠} G) ↾_{𝑠} F = L ↾_{𝑠} F$
68	65 67	eqtrid	$⊢ φ \to I ↾_{𝑠} F = L ↾_{𝑠} F$
69	64 68	eqtr4d	$⊢ φ \to E ↾_{𝑠} F = I ↾_{𝑠} F$
70		eqid	$⊢ I ↾_{𝑠} F = I ↾_{𝑠} F$
71	70	sdrgdrng	$⊢ F \in SubDRing (I) \to I ↾_{𝑠} F \in DivRing$
72	5 71	syl	$⊢ φ \to I ↾_{𝑠} F \in DivRing$
73	69 72	eqeltrd	$⊢ φ \to E ↾_{𝑠} F \in DivRing$
74	73	drngringd	$⊢ φ \to E ↾_{𝑠} F \in Ring$
75	12 34 37	fldgenssv	$⊢ φ \to L fldGen (G \cup H) \subseteq {Base}_{L}$
76	10 12	ressbas2	$⊢ L fldGen (G \cup H) \subseteq {Base}_{L} \to L fldGen (G \cup H) = {Base}_{E}$
77	75 76	syl	$⊢ φ \to L fldGen (G \cup H) = {Base}_{E}$
78	61 77	sseqtrd	$⊢ φ \to F \subseteq {Base}_{E}$
79	34	drngringd	$⊢ φ \to L \in Ring$
80	58 60	sstrd	$⊢ φ \to G \subseteq L fldGen (G \cup H)$
81		sdrgsubrg	$⊢ G \in SubDRing (L) \to G \in SubRing (L)$
82		eqid	$⊢ 1_{L} = 1_{L}$
83	82	subrg1cl	$⊢ G \in SubRing (L) \to 1_{L} \in G$
84	7 81 83	3syl	$⊢ φ \to 1_{L} \in G$
85	80 84	sseldd	$⊢ φ \to 1_{L} \in (L fldGen (G \cup H))$
86	10 12 82	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}$
87	79 85 75 86	syl3anc	$⊢ φ \to 1_{L} = 1_{E}$
88	2 12 82	ress1r	$⊢ (L \in Ring \land 1_{L} \in G \land G \subseteq {Base}_{L}) \to 1_{L} = 1_{I}$
89	79 84 36 88	syl3anc	$⊢ φ \to 1_{L} = 1_{I}$
90	87 89	eqtr3d	$⊢ φ \to 1_{E} = 1_{I}$
91		sdrgsubrg	$⊢ F \in SubDRing (I) \to F \in SubRing (I)$
92		eqid	$⊢ 1_{I} = 1_{I}$
93	92	subrg1cl	$⊢ F \in SubRing (I) \to 1_{I} \in F$
94	5 91 93	3syl	$⊢ φ \to 1_{I} \in F$
95	90 94	eqeltrd	$⊢ φ \to 1_{E} \in F$
96		eqid	$⊢ {Base}_{E} = {Base}_{E}$
97		eqid	$⊢ 1_{E} = 1_{E}$
98	96 97	issubrg	$⊢ F \in SubRing (E) \leftrightarrow ((E \in Ring \land E ↾_{𝑠} F \in Ring) \land (F \subseteq {Base}_{E} \land 1_{E} \in F))$
99	48 74 78 95 98	syl22anbrc	$⊢ φ \to F \in SubRing (E)$
100		issdrg	$⊢ F \in SubDRing (E) \leftrightarrow (E \in DivRing \land F \in SubRing (E) \land E ↾_{𝑠} F \in DivRing)$
101	47 99 73 100	syl3anbrc	$⊢ φ \to F \in SubDRing (E)$
102	10 4 38 101 1	fldsdrgfldext2	$⊢ φ \to E /_{FldExt} K$
103		extdgcl	$⊢ E /_{FldExt} K \to E [. : .] K \in ℕ_{0}^{*}$
104	102 103	syl	$⊢ φ \to E [. : .] K \in ℕ_{0}^{*}$
105	11	nnnn0d	$⊢ φ \to I [. : .] K \in ℕ_{0}$
106	105 9	nn0mulcld	$⊢ φ \to [I : K] [J : K] \in ℕ_{0}$
107	1 2 3 4 5 6 7 8 9 10	fldextrspundglemul	$⊢ φ \to E [. : .] K \leq [I : K] \cdot_{𝑒} [J : K]$
108	9	nn0red	$⊢ φ \to J [. : .] K \in ℝ$
109		rexmul	$⊢ (I [. : .] K \in ℝ \land J [. : .] K \in ℝ) \to [I : K] \cdot_{𝑒} [J : K] = [I : K] [J : K]$
110	26 108 109	syl2anc	$⊢ φ \to [I : K] \cdot_{𝑒} [J : K] = [I : K] [J : K]$
111	107 110	breqtrd	$⊢ φ \to E [. : .] K \leq [I : K] [J : K]$
112		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}$
113	104 106 111 112	syl3anc	$⊢ φ \to E [. : .] K \in ℕ_{0}$
114	113	nn0red	$⊢ φ \to E [. : .] K \in ℝ$
115	114	adantr	$⊢ (φ \land E [. : .] I = +∞) \to E [. : .] K \in ℝ$
116	115	renepnfd	$⊢ (φ \land E [. : .] I = +∞) \to E [. : .] K \neq +∞$
117	116	neneqd	$⊢ (φ \land E [. : .] I = +∞) \to \neg E [. : .] K = +∞$
118	33 117	pm2.65da	$⊢ φ \to \neg E [. : .] I = +∞$
119	19 118	olcnd	$⊢ φ \to E [. : .] I \in ℕ_{0}$

Metamath Proof Explorer

Theorem fldextrspundgdvdslem

Proof