extdg1id

Description: If the degree of the extension E /FldExt F is 1 , then E and F are identical. (Contributed by Thierry Arnoux, 6-Aug-2023)

		Ref	Expression
	Assertion	extdg1id	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → 𝐸 = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fldextress	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐹 = ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) )
2	1	adantr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → 𝐹 = ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) )
3		fldextsralvec	⊢ ( 𝐸 /_FldExt 𝐹 → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
4	3	adantr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
5		eqid	⊢ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
6	5	lbsex	⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec → ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ≠ ∅ )
7	4 6	syl	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ≠ ∅ )
8		n0	⊢ ( ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
9	7 8	sylib	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
10		simpr	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
11	5	dimval	⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝑏 ) )
12	4 11	sylan	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝑏 ) )
13		extdgval	⊢ ( 𝐸 /_FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
14	13	adantr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
15		simpr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( 𝐸 [:] 𝐹 ) = 1 )
16	14 15	eqtr3d	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = 1 )
17	16	adantr	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = 1 )
18	12 17	eqtr3d	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( ♯ ‘ 𝑏 ) = 1 )
19		hash1snb	⊢ ( 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝑏 ) = 1 ↔ ∃ 𝑥 𝑏 = { 𝑥 } ) )
20	19	biimpa	⊢ ( ( 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∧ ( ♯ ‘ 𝑏 ) = 1 ) → ∃ 𝑥 𝑏 = { 𝑥 } )
21	10 18 20	syl2anc	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ∃ 𝑥 𝑏 = { 𝑥 } )
22		simpr	⊢ ( ( ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) )
23		simplr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝑏 = { 𝑥 } )
24		eqidd	⊢ ( 𝐸 /_FldExt 𝐹 → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
25		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
26	25	fldextsubrg	⊢ ( 𝐸 /_FldExt 𝐹 → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
27		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
28	27	subrgss	⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
29	26 28	syl	⊢ ( 𝐸 /_FldExt 𝐹 → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
30	24 29	sravsca	⊢ ( 𝐸 /_FldExt 𝐹 → ( ._r ‘ 𝐸 ) = ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
31	30	eqcomd	⊢ ( 𝐸 /_FldExt 𝐹 → ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( ._r ‘ 𝐸 ) )
32	31	ad5antr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑖 ∈ 𝑏 ) → ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( ._r ‘ 𝐸 ) )
33	32	oveqd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑖 ∈ 𝑏 ) → ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) = ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) )
34	23 33	mpteq12dva	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) = ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) )
35	34	oveq2d	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( 𝐸 Σ_g ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) ) )
36		eqid	⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) )
37		fldextfld1	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐸 ∈ Field )
38		isfld	⊢ ( 𝐸 ∈ Field ↔ ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
39	38	simplbi	⊢ ( 𝐸 ∈ Field → 𝐸 ∈ DivRing )
40	37 39	syl	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐸 ∈ DivRing )
41	40	adantr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → 𝐸 ∈ DivRing )
42	26	adantr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
43		eqid	⊢ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) = ( 𝐸 ↾_s ( Base ‘ 𝐹 ) )
44		fldextfld2	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐹 ∈ Field )
45		isfld	⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
46	45	simplbi	⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
47	44 46	syl	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐹 ∈ DivRing )
48	1 47	eqeltrrd	⊢ ( 𝐸 /_FldExt 𝐹 → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing )
49	48	adantr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing )
50		simpr	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
51	36 41 42 43 49 50	drgextgsum	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) )
52	51	adantlr	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) )
53	52	ad2antrr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) )
54		drngring	⊢ ( 𝐸 ∈ DivRing → 𝐸 ∈ Ring )
55	37 39 54	3syl	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐸 ∈ Ring )
56		ringmnd	⊢ ( 𝐸 ∈ Ring → 𝐸 ∈ Mnd )
57	55 56	syl	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐸 ∈ Mnd )
58	57	ad4antr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝐸 ∈ Mnd )
59		vex	⊢ 𝑥 ∈ V
60	59	a1i	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝑥 ∈ V )
61	55	ad3antrrr	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝐸 ∈ Ring )
62	61	adantr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝐸 ∈ Ring )
63	29	ad3antrrr	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
64	63	adantr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
65		elmapi	⊢ ( 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) → 𝑣 : 𝑏 ⟶ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) )
66	65	adantl	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝑣 : 𝑏 ⟶ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) )
67		vsnid	⊢ 𝑥 ∈ { 𝑥 }
68	67 23	eleqtrrid	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝑥 ∈ 𝑏 )
69	66 68	ffvelcdmd	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) )
70	24 29	srasca	⊢ ( 𝐸 /_FldExt 𝐹 → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
71	1 70	eqtrd	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐹 = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
72	71	fveq2d	⊢ ( 𝐸 /_FldExt 𝐹 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) )
73	72	ad4antr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) )
74	69 73	eleqtrrd	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
75	64 74	sseldd	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
76		simpr	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝑏 = { 𝑥 } )
77		simplr	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
78		eqid	⊢ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
79	78 5	lbsss	⊢ ( 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) → 𝑏 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
80	77 79	syl	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝑏 ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
81	76 80	eqsstrrd	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → { 𝑥 } ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
82	59	snss	⊢ ( 𝑥 ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ↔ { 𝑥 } ⊆ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
83	81 82	sylibr	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝑥 ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
84		eqidd	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
85	84 63	srabase	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( Base ‘ 𝐸 ) = ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
86	83 85	eleqtrrd	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
87	86	adantr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
88		eqid	⊢ ( ._r ‘ 𝐸 ) = ( ._r ‘ 𝐸 )
89	27 88	ringcl	⊢ ( ( 𝐸 ∈ Ring ∧ ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
90	62 75 87 89	syl3anc	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
91		simpr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑖 = 𝑥 ) → 𝑖 = 𝑥 )
92	91	fveq2d	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑖 = 𝑥 ) → ( 𝑣 ‘ 𝑖 ) = ( 𝑣 ‘ 𝑥 ) )
93	92 91	oveq12d	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑖 = 𝑥 ) → ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
94	27 58 60 90 93	gsumsnd	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
95	1	fveq2d	⊢ ( 𝐸 /_FldExt 𝐹 → ( ._r ‘ 𝐹 ) = ( ._r ‘ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ) )
96	43 88	ressmulr	⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) → ( ._r ‘ 𝐸 ) = ( ._r ‘ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ) )
97	26 96	syl	⊢ ( 𝐸 /_FldExt 𝐹 → ( ._r ‘ 𝐸 ) = ( ._r ‘ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ) )
98	95 97	eqtr4d	⊢ ( 𝐸 /_FldExt 𝐹 → ( ._r ‘ 𝐹 ) = ( ._r ‘ 𝐸 ) )
99	98	ad4antr	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ._r ‘ 𝐹 ) = ( ._r ‘ 𝐸 ) )
100	99	oveqd	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐹 ) 𝑥 ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
101	94 100	eqtr4d	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐹 ) 𝑥 ) )
102	35 53 101	3eqtr3d	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐹 ) 𝑥 ) )
103	102	adantlr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐹 ) 𝑥 ) )
104		drngring	⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
105	44 46 104	3syl	⊢ ( 𝐸 /_FldExt 𝐹 → 𝐹 ∈ Ring )
106	105	ad5antr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝐹 ∈ Ring )
107	74	adantlr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
108		eqid	⊢ ( 1_r ‘ 𝐸 ) = ( 1_r ‘ 𝐸 )
109		eqid	⊢ ( Unit ‘ 𝐸 ) = ( Unit ‘ 𝐸 )
110		eqid	⊢ ( inv_r ‘ 𝐸 ) = ( inv_r ‘ 𝐸 )
111		simp-5l	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 /_FldExt 𝐹 )
112	111 55	syl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 ∈ Ring )
113	87	adantr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
114	75	adantr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
115	38	simprbi	⊢ ( 𝐸 ∈ Field → 𝐸 ∈ CRing )
116	111 37 115	3syl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 ∈ CRing )
117	27 88	crngcom	⊢ ( ( 𝐸 ∈ CRing ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) ) → ( 𝑥 ( ._r ‘ 𝐸 ) ( 𝑣 ‘ 𝑥 ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
118	116 113 114 117	syl3anc	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑥 ( ._r ‘ 𝐸 ) ( 𝑣 ‘ 𝑥 ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
119		simpr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) )
120	52	ad3antrrr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) )
121	34	adantr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) = ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) )
122	121	oveq2d	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) = ( 𝐸 Σ_g ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) ) )
123	119 120 122	3eqtr2d	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 1_r ‘ 𝐸 ) = ( 𝐸 Σ_g ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) ) )
124	94	adantr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝐸 Σ_g ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( ._r ‘ 𝐸 ) 𝑖 ) ) ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
125	123 124	eqtrd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 1_r ‘ 𝐸 ) = ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) )
126	118 125	eqtr4d	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑥 ( ._r ‘ 𝐸 ) ( 𝑣 ‘ 𝑥 ) ) = ( 1_r ‘ 𝐸 ) )
127	125	eqcomd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐸 ) 𝑥 ) = ( 1_r ‘ 𝐸 ) )
128	27 88 108 109 110 112 113 114 126 127	invrvald	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑥 ∈ ( Unit ‘ 𝐸 ) ∧ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) = ( 𝑣 ‘ 𝑥 ) ) )
129	128	simpld	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ∈ ( Unit ‘ 𝐸 ) )
130	109 110	unitinvinv	⊢ ( ( 𝐸 ∈ Ring ∧ 𝑥 ∈ ( Unit ‘ 𝐸 ) ) → ( ( inv_r ‘ 𝐸 ) ‘ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ) = 𝑥 )
131	62 129 130	syl2an2r	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( inv_r ‘ 𝐸 ) ‘ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ) = 𝑥 )
132	111 37 39	3syl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 ∈ DivRing )
133	111 26	syl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
134	111 1	syl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐹 = ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) )
135	111 44 46	3syl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐹 ∈ DivRing )
136	134 135	eqeltrrd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing )
137	128	simprd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) = ( 𝑣 ‘ 𝑥 ) )
138	74	adantr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
139	137 138	eqeltrd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
140		eqidd	⊢ ( 𝐸 /_FldExt 𝐹 → ( 0_g ‘ 𝐸 ) = ( 0_g ‘ 𝐸 ) )
141	24 140 29	sralmod0	⊢ ( 𝐸 /_FldExt 𝐹 → ( 0_g ‘ 𝐸 ) = ( 0_g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
142	141	ad2antrr	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( 0_g ‘ 𝐸 ) = ( 0_g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
143	5	lbslinds	⊢ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ⊆ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
144	143 10	sselid	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → 𝑏 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
145		eqid	⊢ ( 0_g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( 0_g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
146	145	0nellinds	⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec ∧ 𝑏 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ¬ ( 0_g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ 𝑏 )
147	4 144 146	syl2an2r	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ¬ ( 0_g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ 𝑏 )
148	142 147	eqneltrd	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ¬ ( 0_g ‘ 𝐸 ) ∈ 𝑏 )
149	148	ad3antrrr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ¬ ( 0_g ‘ 𝐸 ) ∈ 𝑏 )
150		nelne2	⊢ ( ( 𝑥 ∈ 𝑏 ∧ ¬ ( 0_g ‘ 𝐸 ) ∈ 𝑏 ) → 𝑥 ≠ ( 0_g ‘ 𝐸 ) )
151	68 149 150	syl2an2r	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ≠ ( 0_g ‘ 𝐸 ) )
152		eqid	⊢ ( 0_g ‘ 𝐸 ) = ( 0_g ‘ 𝐸 )
153	27 152 110	drnginvrn0	⊢ ( ( 𝐸 ∈ DivRing ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑥 ≠ ( 0_g ‘ 𝐸 ) ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ≠ ( 0_g ‘ 𝐸 ) )
154	132 113 151 153	syl3anc	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ≠ ( 0_g ‘ 𝐸 ) )
155		eldifsn	⊢ ( ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ↔ ( ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ∧ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ≠ ( 0_g ‘ 𝐸 ) ) )
156	139 154 155	sylanbrc	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) )
157		fveq2	⊢ ( 𝑎 = ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑎 ) = ( ( inv_r ‘ 𝐸 ) ‘ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ) )
158	157	eleq1d	⊢ ( 𝑎 = ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) → ( ( ( inv_r ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) ↔ ( ( inv_r ‘ 𝐸 ) ‘ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐹 ) ) )
159	43 152 110	issubdrg	⊢ ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) → ( ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing ↔ ∀ 𝑎 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ( ( inv_r ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) ) )
160	159	biimpa	⊢ ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing ) → ∀ 𝑎 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ( ( inv_r ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) )
161	160	adantr	⊢ ( ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing ) ∧ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ) → ∀ 𝑎 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ( ( inv_r ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) )
162		simpr	⊢ ( ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing ) ∧ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) )
163	158 161 162	rspcdva	⊢ ( ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) ∈ DivRing ) ∧ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( inv_r ‘ 𝐸 ) ‘ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐹 ) )
164	132 133 136 156 163	syl1111anc	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( inv_r ‘ 𝐸 ) ‘ ( ( inv_r ‘ 𝐸 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐹 ) )
165	131 164	eqeltrrd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
166	165	adantrl	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
167	27 108	ringidcl	⊢ ( 𝐸 ∈ Ring → ( 1_r ‘ 𝐸 ) ∈ ( Base ‘ 𝐸 ) )
168	61 167	syl	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 1_r ‘ 𝐸 ) ∈ ( Base ‘ 𝐸 ) )
169	168 85	eleqtrd	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 1_r ‘ 𝐸 ) ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
170		eqid	⊢ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
171		eqid	⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
172		eqid	⊢ ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) = ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
173		eqid	⊢ ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
174	4	ad2antrr	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
175		lveclmod	⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LMod )
176	174 175	syl	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LMod )
177	78 170 171 172 173 176 77	lbslsp	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( ( 1_r ‘ 𝐸 ) ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ↔ ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) )
178	169 177	mpbid	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ ( 1_r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) )
179	166 178	r19.29a	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
180	179	ad2antrr	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
181		eqid	⊢ ( ._r ‘ 𝐹 ) = ( ._r ‘ 𝐹 )
182	25 181	ringcl	⊢ ( ( 𝐹 ∈ Ring ∧ ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐹 ) 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
183	106 107 180 182	syl3anc	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ( 𝑣 ‘ 𝑥 ) ( ._r ‘ 𝐹 ) 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
184	103 183	eqeltrd	⊢ ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) → ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ∈ ( Base ‘ 𝐹 ) )
185	184	ad2antrr	⊢ ( ( ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ∈ ( Base ‘ 𝐹 ) )
186	22 185	eqeltrd	⊢ ( ( ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑢 ∈ ( Base ‘ 𝐹 ) )
187	186	anasss	⊢ ( ( ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ) ∧ ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) → 𝑢 ∈ ( Base ‘ 𝐹 ) )
188	85	eleq2d	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 𝑢 ∈ ( Base ‘ 𝐸 ) ↔ 𝑢 ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) )
189	78 170 171 172 173 176 77	lbslsp	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 𝑢 ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ↔ ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) )
190	188 189	bitrd	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 𝑢 ∈ ( Base ‘ 𝐸 ) ↔ ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) )
191	190	biimpa	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) → ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑_m 𝑏 ) ( 𝑣 finSupp ( 0_g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σ_g ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·_𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) )
192	187 191	r19.29a	⊢ ( ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) → 𝑢 ∈ ( Base ‘ 𝐹 ) )
193	192	ex	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 𝑢 ∈ ( Base ‘ 𝐸 ) → 𝑢 ∈ ( Base ‘ 𝐹 ) ) )
194	193	ssrdv	⊢ ( ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) )
195	21 194	exlimddv	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) )
196	9 195	exlimddv	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) )
197		simpr	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) ) → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) )
198	37	ad2antrr	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) ) → 𝐸 ∈ Field )
199		fvexd	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) ) → ( Base ‘ 𝐹 ) ∈ V )
200	43 27	ressid2	⊢ ( ( ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) ∧ 𝐸 ∈ Field ∧ ( Base ‘ 𝐹 ) ∈ V ) → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) = 𝐸 )
201	197 198 199 200	syl3anc	⊢ ( ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐹 ) ) → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) = 𝐸 )
202	196 201	mpdan	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → ( 𝐸 ↾_s ( Base ‘ 𝐹 ) ) = 𝐸 )
203	2 202	eqtr2d	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → 𝐸 = 𝐹 )

Metamath Proof Explorer

Theorem extdg1id

Proof