| 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 ( 0g ‘ ( 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 |
⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 ) |
| 109 |
|
eqid |
⊢ ( Unit ‘ 𝐸 ) = ( Unit ‘ 𝐸 ) |
| 110 |
|
eqid |
⊢ ( invr ‘ 𝐸 ) = ( invr ‘ 𝐸 ) |
| 111 |
|
simp-5l |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 /FldExt 𝐹 ) |
| 112 |
111 55
|
syl |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 ∈ Ring ) |
| 113 |
87
|
adantr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) ) |
| 114 |
75
|
adantr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( 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 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( 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 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑥 ( .r ‘ 𝐸 ) ( 𝑣 ‘ 𝑥 ) ) = ( ( 𝑣 ‘ 𝑥 ) ( .r ‘ 𝐸 ) 𝑥 ) ) |
| 119 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) |
| 120 |
52
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( 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 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) = ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) |
| 122 |
121
|
oveq2d |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( 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 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 1r ‘ 𝐸 ) = ( 𝐸 Σg ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) ) |
| 124 |
94
|
adantr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝐸 Σg ( 𝑖 ∈ { 𝑥 } ↦ ( ( 𝑣 ‘ 𝑖 ) ( .r ‘ 𝐸 ) 𝑖 ) ) ) = ( ( 𝑣 ‘ 𝑥 ) ( .r ‘ 𝐸 ) 𝑥 ) ) |
| 125 |
123 124
|
eqtrd |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 1r ‘ 𝐸 ) = ( ( 𝑣 ‘ 𝑥 ) ( .r ‘ 𝐸 ) 𝑥 ) ) |
| 126 |
118 125
|
eqtr4d |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑥 ( .r ‘ 𝐸 ) ( 𝑣 ‘ 𝑥 ) ) = ( 1r ‘ 𝐸 ) ) |
| 127 |
125
|
eqcomd |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( 𝑣 ‘ 𝑥 ) ( .r ‘ 𝐸 ) 𝑥 ) = ( 1r ‘ 𝐸 ) ) |
| 128 |
27 88 108 109 110 112 113 114 126 127
|
invrvald |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑥 ∈ ( Unit ‘ 𝐸 ) ∧ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) = ( 𝑣 ‘ 𝑥 ) ) ) |
| 129 |
128
|
simpld |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ∈ ( Unit ‘ 𝐸 ) ) |
| 130 |
109 110
|
unitinvinv |
⊢ ( ( 𝐸 ∈ Ring ∧ 𝑥 ∈ ( Unit ‘ 𝐸 ) ) → ( ( invr ‘ 𝐸 ) ‘ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ) = 𝑥 ) |
| 131 |
62 129 130
|
syl2an2r |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( invr ‘ 𝐸 ) ‘ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ) = 𝑥 ) |
| 132 |
111 37 39
|
3syl |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐸 ∈ DivRing ) |
| 133 |
111 26
|
syl |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) |
| 134 |
111 1
|
syl |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) |
| 135 |
111 44 46
|
3syl |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝐹 ∈ DivRing ) |
| 136 |
134 135
|
eqeltrrd |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ) |
| 137 |
128
|
simprd |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) = ( 𝑣 ‘ 𝑥 ) ) |
| 138 |
74
|
adantr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( 𝑣 ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) |
| 139 |
137 138
|
eqeltrd |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) |
| 140 |
|
eqidd |
⊢ ( 𝐸 /FldExt 𝐹 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 ) ) |
| 141 |
24 140 29
|
sralmod0 |
⊢ ( 𝐸 /FldExt 𝐹 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) |
| 142 |
141
|
ad2antrr |
⊢ ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( ( 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 |
⊢ ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) |
| 146 |
145
|
0nellinds |
⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec ∧ 𝑏 ∈ ( LIndS ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ¬ ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ 𝑏 ) |
| 147 |
4 144 146
|
syl2an2r |
⊢ ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ¬ ( 0g ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ 𝑏 ) |
| 148 |
142 147
|
eqneltrd |
⊢ ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) → ¬ ( 0g ‘ 𝐸 ) ∈ 𝑏 ) |
| 149 |
148
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ¬ ( 0g ‘ 𝐸 ) ∈ 𝑏 ) |
| 150 |
|
nelne2 |
⊢ ( ( 𝑥 ∈ 𝑏 ∧ ¬ ( 0g ‘ 𝐸 ) ∈ 𝑏 ) → 𝑥 ≠ ( 0g ‘ 𝐸 ) ) |
| 151 |
68 149 150
|
syl2an2r |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ≠ ( 0g ‘ 𝐸 ) ) |
| 152 |
|
eqid |
⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 ) |
| 153 |
27 152 110
|
drnginvrn0 |
⊢ ( ( 𝐸 ∈ DivRing ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑥 ≠ ( 0g ‘ 𝐸 ) ) → ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐸 ) ) |
| 154 |
132 113 151 153
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐸 ) ) |
| 155 |
|
eldifsn |
⊢ ( ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ↔ ( ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ∧ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝐸 ) ) ) |
| 156 |
139 154 155
|
sylanbrc |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ) |
| 157 |
|
fveq2 |
⊢ ( 𝑎 = ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) → ( ( invr ‘ 𝐸 ) ‘ 𝑎 ) = ( ( invr ‘ 𝐸 ) ‘ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ) ) |
| 158 |
157
|
eleq1d |
⊢ ( 𝑎 = ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) → ( ( ( invr ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) ↔ ( ( invr ‘ 𝐸 ) ‘ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐹 ) ) ) |
| 159 |
43 152 110
|
issubdrg |
⊢ ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) → ( ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ↔ ∀ 𝑎 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ( ( invr ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) ) ) |
| 160 |
159
|
biimpa |
⊢ ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ) → ∀ 𝑎 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ( ( invr ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) ) |
| 161 |
160
|
adantr |
⊢ ( ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ) ∧ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ) → ∀ 𝑎 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ( ( invr ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝐹 ) ) |
| 162 |
|
simpr |
⊢ ( ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ) ∧ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ) → ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ) |
| 163 |
158 161 162
|
rspcdva |
⊢ ( ( ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ∧ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ) ∧ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g ‘ 𝐸 ) } ) ) → ( ( invr ‘ 𝐸 ) ‘ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐹 ) ) |
| 164 |
132 133 136 156 163
|
syl1111anc |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → ( ( invr ‘ 𝐸 ) ‘ ( ( invr ‘ 𝐸 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐹 ) ) |
| 165 |
131 164
|
eqeltrrd |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) ) |
| 166 |
165
|
adantrl |
⊢ ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 𝑣 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) ) |
| 167 |
27 108
|
ringidcl |
⊢ ( 𝐸 ∈ Ring → ( 1r ‘ 𝐸 ) ∈ ( Base ‘ 𝐸 ) ) |
| 168 |
61 167
|
syl |
⊢ ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 1r ‘ 𝐸 ) ∈ ( Base ‘ 𝐸 ) ) |
| 169 |
168 85
|
eleqtrd |
⊢ ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 1r ‘ 𝐸 ) ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) |
| 170 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) |
| 171 |
|
eqid |
⊢ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) = ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) |
| 172 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) = ( 0g ‘ ( 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 ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( ( 1r ‘ 𝐸 ) ∈ ( Base ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ↔ ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ( 𝑣 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) ) |
| 178 |
169 177
|
mpbid |
⊢ ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ( 𝑣 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ ( 1r ‘ 𝐸 ) = ( ( ( 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 ( 0g ‘ ( 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 ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) → 𝑢 ∈ ( Base ‘ 𝐹 ) ) |
| 187 |
186
|
anasss |
⊢ ( ( ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) ∧ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ) ∧ ( 𝑣 finSupp ( 0g ‘ ( 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 ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) ) |
| 190 |
188 189
|
bitrd |
⊢ ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) → ( 𝑢 ∈ ( Base ‘ 𝐸 ) ↔ ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ( 𝑣 finSupp ( 0g ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑢 = ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) Σg ( 𝑖 ∈ 𝑏 ↦ ( ( 𝑣 ‘ 𝑖 ) ( ·𝑠 ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) 𝑖 ) ) ) ) ) ) |
| 191 |
190
|
biimpa |
⊢ ( ( ( ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) ∧ 𝑏 ∈ ( LBasis ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ∧ 𝑏 = { 𝑥 } ) ∧ 𝑢 ∈ ( Base ‘ 𝐸 ) ) → ∃ 𝑣 ∈ ( ( Base ‘ ( Scalar ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) ↑m 𝑏 ) ( 𝑣 finSupp ( 0g ‘ ( 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 ) → 𝐸 = 𝐹 ) |