Step | Hyp | Ref
| Expression |
1 | | fldextress 31727 |
. . 3
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) |
2 | 1 | adantr 481 |
. 2
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐹 = (𝐸 ↾s (Base‘𝐹))) |
3 | | fldextsralvec 31730 |
. . . . . . 7
⊢ (𝐸/FldExt𝐹 → ((subringAlg
‘𝐸)‘(Base‘𝐹)) ∈ LVec) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec) |
5 | | eqid 2738 |
. . . . . . 7
⊢
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹))) |
6 | 5 | lbsex 20427 |
. . . . . 6
⊢
(((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec →
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅) |
7 | 4, 6 | syl 17 |
. . . . 5
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹))) ≠ ∅) |
8 | | n0 4280 |
. . . . 5
⊢
((LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
9 | 7, 8 | sylib 217 |
. . . 4
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ∃𝑏 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
10 | | simpr 485 |
. . . . . 6
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
11 | 5 | dimval 31686 |
. . . . . . . 8
⊢
((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏)) |
12 | 4, 11 | sylan 580 |
. . . . . . 7
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏)) |
13 | | extdgval 31729 |
. . . . . . . . . 10
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
14 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
15 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = 1) |
16 | 14, 15 | eqtr3d 2780 |
. . . . . . . 8
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = 1) |
17 | 16 | adantr 481 |
. . . . . . 7
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = 1) |
18 | 12, 17 | eqtr3d 2780 |
. . . . . 6
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (♯‘𝑏) = 1) |
19 | | hash1snb 14134 |
. . . . . . 7
⊢ (𝑏 ∈
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → ((♯‘𝑏) = 1 ↔ ∃𝑥 𝑏 = {𝑥})) |
20 | 19 | biimpa 477 |
. . . . . 6
⊢ ((𝑏 ∈
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∧ (♯‘𝑏) = 1) → ∃𝑥 𝑏 = {𝑥}) |
21 | 10, 18, 20 | syl2anc 584 |
. . . . 5
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ∃𝑥 𝑏 = {𝑥}) |
22 | | simpr 485 |
. . . . . . . . . 10
⊢
((((((((𝐸/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 766 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑏 = {𝑥}) |
24 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → ((subringAlg
‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹))) |
25 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝐹) =
(Base‘𝐹) |
26 | 25 | fldextsubrg 31726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸/FldExt𝐹 → (Base‘𝐹) ∈ (SubRing‘𝐸)) |
27 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝐸) =
(Base‘𝐸) |
28 | 27 | subrgss 20025 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((Base‘𝐹)
∈ (SubRing‘𝐸)
→ (Base‘𝐹)
⊆ (Base‘𝐸)) |
29 | 26, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → (Base‘𝐹) ⊆ (Base‘𝐸)) |
30 | 24, 29 | sravsca 20449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐸) = (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
31 | 30 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r‘𝐸)) |
32 | 31 | ad5antr 731 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 ∈ 𝑏) → (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r‘𝐸)) |
33 | 32 | oveqd 7292 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 ∈ 𝑏) → ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖) = ((𝑣‘𝑖)(.r‘𝐸)𝑖)) |
34 | 23, 33 | mpteq12dva 5163 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) |
35 | 34 | oveq2d 7291 |
. . . . . . . . . . . . . 14
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖)))) |
36 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹)) |
37 | | fldextfld1 31724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) |
38 | | isfld 20000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸 ∈ Field ↔ (𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing)) |
39 | 38 | simplbi 498 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸 ∈ Field → 𝐸 ∈
DivRing) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ DivRing) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝐸 ∈ DivRing) |
42 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (Base‘𝐹) ∈ (SubRing‘𝐸)) |
43 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 ↾s
(Base‘𝐹)) = (𝐸 ↾s
(Base‘𝐹)) |
44 | | fldextfld2 31725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) |
45 | | isfld 20000 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ∈ Field ↔ (𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing)) |
46 | 45 | simplbi 498 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ Field → 𝐹 ∈
DivRing) |
47 | 44, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ DivRing) |
48 | 1, 47 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → (𝐸 ↾s (Base‘𝐹)) ∈
DivRing) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (𝐸 ↾s (Base‘𝐹)) ∈
DivRing) |
50 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
51 | 36, 41, 42, 43, 49, 50 | drgextgsum 31682 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) |
52 | 51 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) |
53 | 52 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) |
54 | | drngring 19998 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring) |
55 | 37, 39, 54 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Ring) |
56 | | ringmnd 19793 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Mnd) |
58 | 57 | ad4antr 729 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Mnd) |
59 | | vex 3436 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ V) |
61 | 55 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝐸 ∈ Ring) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Ring) |
63 | 29 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐹) ⊆ (Base‘𝐸)) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) ⊆ (Base‘𝐸)) |
65 | | elmapi 8637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏) → 𝑣:𝑏⟶(Base‘(Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))))) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑣:𝑏⟶(Base‘(Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))))) |
67 | | vsnid 4598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ {𝑥} |
68 | 67, 23 | eleqtrrid 2846 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ 𝑏) |
69 | 66, 68 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) |
70 | 24, 29 | srasca 20447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸/FldExt𝐹 → (𝐸 ↾s (Base‘𝐹)) = (Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
71 | 1, 70 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸/FldExt𝐹 → 𝐹 = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
72 | 71 | fveq2d 6778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → (Base‘𝐹) =
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) |
73 | 72 | ad4antr 729 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) = (Base‘(Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))))) |
74 | 69, 73 | eleqtrrd 2842 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈ (Base‘𝐹)) |
75 | 64, 74 | sseldd 3922 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈ (Base‘𝐸)) |
76 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 = {𝑥}) |
77 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
78 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) |
79 | 78, 5 | lbsss 20339 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
81 | 76, 80 | eqsstrrd 3960 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → {𝑥} ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
82 | 59 | snss 4719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹))) ↔ {𝑥} ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
83 | 81, 82 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
84 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹))) |
85 | 84, 63 | srabase 20441 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
86 | 83, 85 | eleqtrrd 2842 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐸)) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐸)) |
88 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(.r‘𝐸) = (.r‘𝐸) |
89 | 27, 88 | ringcl 19800 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 ∈ Ring ∧ (𝑣‘𝑥) ∈ (Base‘𝐸) ∧ 𝑥 ∈ (Base‘𝐸)) → ((𝑣‘𝑥)(.r‘𝐸)𝑥) ∈ (Base‘𝐸)) |
90 | 62, 75, 87, 89 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣‘𝑥)(.r‘𝐸)𝑥) ∈ (Base‘𝐸)) |
91 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → 𝑖 = 𝑥) |
92 | 91 | fveq2d 6778 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → (𝑣‘𝑖) = (𝑣‘𝑥)) |
93 | 92, 91 | oveq12d 7293 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → ((𝑣‘𝑖)(.r‘𝐸)𝑖) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
94 | 27, 58, 60, 90, 93 | gsumsnd 19553 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
95 | 1 | fveq2d 6778 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐹) =
(.r‘(𝐸
↾s (Base‘𝐹)))) |
96 | 43, 88 | ressmulr 17017 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Base‘𝐹)
∈ (SubRing‘𝐸)
→ (.r‘𝐸) = (.r‘(𝐸 ↾s (Base‘𝐹)))) |
97 | 26, 96 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐸) =
(.r‘(𝐸
↾s (Base‘𝐹)))) |
98 | 95, 97 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐹) =
(.r‘𝐸)) |
99 | 98 | ad4antr 729 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (.r‘𝐹) = (.r‘𝐸)) |
100 | 99 | oveqd 7292 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣‘𝑥)(.r‘𝐹)𝑥) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
101 | 94, 100 | eqtr4d 2781 |
. . . . . . . . . . . . . 14
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) = ((𝑣‘𝑥)(.r‘𝐹)𝑥)) |
102 | 35, 53, 101 | 3eqtr3d 2786 |
. . . . . . . . . . . . 13
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣‘𝑥)(.r‘𝐹)𝑥)) |
103 | 102 | adantlr 712 |
. . . . . . . . . . . 12
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣‘𝑥)(.r‘𝐹)𝑥)) |
104 | | drngring 19998 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ DivRing → 𝐹 ∈ Ring) |
105 | 44, 46, 104 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Ring) |
106 | 105 | ad5antr 731 |
. . . . . . . . . . . . 13
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐹 ∈ Ring) |
107 | 74 | adantlr 712 |
. . . . . . . . . . . . 13
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈ (Base‘𝐹)) |
108 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘𝐸) = (1r‘𝐸) |
109 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Unit‘𝐸) =
(Unit‘𝐸) |
110 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(invr‘𝐸) = (invr‘𝐸) |
111 | | simp-5l 782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸/FldExt𝐹) |
112 | 111, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ Ring) |
113 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐸)) |
114 | 75 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑣‘𝑥) ∈ (Base‘𝐸)) |
115 | 38 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐸 ∈ Field → 𝐸 ∈ CRing) |
116 | 111, 37, 115 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ CRing) |
117 | 27, 88 | crngcom 19801 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ CRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ (𝑣‘𝑥) ∈ (Base‘𝐸)) → (𝑥(.r‘𝐸)(𝑣‘𝑥)) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
118 | 116, 113,
114, 117 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r‘𝐸)(𝑣‘𝑥)) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
119 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐸/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 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐸/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 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) |
122 | 121 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐸/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 2784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r‘𝐸) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖)))) |
124 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
125 | 123, 124 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r‘𝐸) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) |
126 | 118, 125 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r‘𝐸)(𝑣‘𝑥)) = (1r‘𝐸)) |
127 | 125 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/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 21825 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥 ∈ (Unit‘𝐸) ∧ ((invr‘𝐸)‘𝑥) = (𝑣‘𝑥))) |
129 | 128 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Unit‘𝐸)) |
130 | 109, 110 | unitinvinv 19917 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 ∈ Ring ∧ 𝑥 ∈ (Unit‘𝐸)) →
((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) = 𝑥) |
131 | 62, 129, 130 | syl2an2r 682 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) = 𝑥) |
132 | 111, 37, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ DivRing) |
133 | 111, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (Base‘𝐹) ∈ (SubRing‘𝐸)) |
134 | 111, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐹 = (𝐸 ↾s (Base‘𝐹))) |
135 | 111, 44, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐹 ∈ DivRing) |
136 | 134, 135 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 ↾s (Base‘𝐹)) ∈
DivRing) |
137 | 128 | simprd 496 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) = (𝑣‘𝑥)) |
138 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑣‘𝑥) ∈ (Base‘𝐹)) |
139 | 137, 138 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) ∈ (Base‘𝐹)) |
140 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐸/FldExt𝐹 →
(0g‘𝐸) =
(0g‘𝐸)) |
141 | 24, 140, 29 | sralmod0 20458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐸/FldExt𝐹 →
(0g‘𝐸) =
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
142 | 141 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (0g‘𝐸) =
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
143 | 5 | lbslinds 21040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ⊆ (LIndS‘((subringAlg
‘𝐸)‘(Base‘𝐹))) |
144 | 143, 10 | sselid 3919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LIndS‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) |
145 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (0g‘((subringAlg
‘𝐸)‘(Base‘𝐹))) |
146 | 145 | 0nellinds 31566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LIndS‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ¬
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏) |
147 | 4, 144, 146 | syl2an2r 682 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ¬
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏) |
148 | 142, 147 | eqneltrd 2858 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ¬ (0g‘𝐸) ∈ 𝑏) |
149 | 148 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ¬ (0g‘𝐸) ∈ 𝑏) |
150 | | nelne2 3042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝑏 ∧ ¬ (0g‘𝐸) ∈ 𝑏) → 𝑥 ≠ (0g‘𝐸)) |
151 | 68, 149, 150 | syl2an2r 682 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ≠ (0g‘𝐸)) |
152 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘𝐸) = (0g‘𝐸) |
153 | 27, 152, 110 | drnginvrn0 20009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 ∈ DivRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ 𝑥 ≠ (0g‘𝐸)) → ((invr‘𝐸)‘𝑥) ≠ (0g‘𝐸)) |
154 | 132, 113,
151, 153 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) ≠ (0g‘𝐸)) |
155 | | eldifsn 4720 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)}) ↔
(((invr‘𝐸)‘𝑥) ∈ (Base‘𝐹) ∧ ((invr‘𝐸)‘𝑥) ≠ (0g‘𝐸))) |
156 | 139, 154,
155 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) |
157 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = ((invr‘𝐸)‘𝑥) → ((invr‘𝐸)‘𝑎) = ((invr‘𝐸)‘((invr‘𝐸)‘𝑥))) |
158 | 157 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ((invr‘𝐸)‘𝑥) → (((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹) ↔ ((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) ∈ (Base‘𝐹))) |
159 | 43, 152, 110 | issubdrg 20049 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) →
((𝐸 ↾s
(Base‘𝐹)) ∈
DivRing ↔ ∀𝑎
∈ ((Base‘𝐹)
∖ {(0g‘𝐸)})((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹))) |
160 | 159 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) → ∀𝑎
∈ ((Base‘𝐹)
∖ {(0g‘𝐸)})((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹)) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) ∧ ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) → ∀𝑎 ∈ ((Base‘𝐹) ∖
{(0g‘𝐸)})((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹)) |
162 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) ∧ ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) →
((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) |
163 | 158, 161,
162 | rspcdva 3562 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) ∧ ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) →
((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) ∈ (Base‘𝐹)) |
164 | 132, 133,
136, 156, 163 | syl1111anc 837 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) ∈ (Base‘𝐹)) |
165 | 131, 164 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐹)) |
166 | 165 | adantrl 713 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐸/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 19807 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∈ Ring →
(1r‘𝐸)
∈ (Base‘𝐸)) |
168 | 61, 167 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r‘𝐸) ∈ (Base‘𝐸)) |
169 | 168, 85 | eleqtrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r‘𝐸) ∈
(Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
170 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) =
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
171 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))) |
172 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) =
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) |
173 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) |
174 | 4 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec) |
175 | | lveclmod 20368 |
. . . . . . . . . . . . . . . . . 18
⊢
(((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec → ((subringAlg
‘𝐸)‘(Base‘𝐹)) ∈ LMod) |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LMod) |
177 | 78, 170, 171, 172, 173, 176, 77 | lbslsp 31572 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐸/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 231 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐸/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 3218 |
. . . . . . . . . . . . . 14
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐹)) |
180 | 179 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐹)) |
181 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝐹) = (.r‘𝐹) |
182 | 25, 181 | ringcl 19800 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Ring ∧ (𝑣‘𝑥) ∈ (Base‘𝐹) ∧ 𝑥 ∈ (Base‘𝐹)) → ((𝑣‘𝑥)(.r‘𝐹)𝑥) ∈ (Base‘𝐹)) |
183 | 106, 107,
180, 182 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣‘𝑥)(.r‘𝐹)𝑥) ∈ (Base‘𝐹)) |
184 | 103, 183 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) ∈ (Base‘𝐹)) |
185 | 184 | ad2antrr 723 |
. . . . . . . . . 10
⊢
((((((((𝐸/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 2839 |
. . . . . . . . 9
⊢
((((((((𝐸/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 467 |
. . . . . . . 8
⊢
(((((((𝐸/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 2824 |
. . . . . . . . . 10
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ 𝑢 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) |
189 | 78, 170, 171, 172, 173, 176, 77 | lbslsp 31572 |
. . . . . . . . . 10
⊢ ((((𝐸/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 278 |
. . . . . . . . 9
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ ∃𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))))) |
191 | 190 | biimpa 477 |
. . . . . . . 8
⊢
(((((𝐸/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 3218 |
. . . . . . 7
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) → 𝑢 ∈ (Base‘𝐹)) |
193 | 192 | ex 413 |
. . . . . 6
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) → 𝑢 ∈ (Base‘𝐹))) |
194 | 193 | ssrdv 3927 |
. . . . 5
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) ⊆ (Base‘𝐹)) |
195 | 21, 194 | exlimddv 1938 |
. . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (Base‘𝐸) ⊆ (Base‘𝐹)) |
196 | 9, 195 | exlimddv 1938 |
. . 3
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (Base‘𝐸) ⊆ (Base‘𝐹)) |
197 | | simpr 485 |
. . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐸) ⊆ (Base‘𝐹)) |
198 | 37 | ad2antrr 723 |
. . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → 𝐸 ∈ Field) |
199 | | fvexd 6789 |
. . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐹) ∈ V) |
200 | 43, 27 | ressid2 16945 |
. . . 4
⊢
(((Base‘𝐸)
⊆ (Base‘𝐹)
∧ 𝐸 ∈ Field ∧
(Base‘𝐹) ∈ V)
→ (𝐸
↾s (Base‘𝐹)) = 𝐸) |
201 | 197, 198,
199, 200 | syl3anc 1370 |
. . 3
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (𝐸 ↾s (Base‘𝐹)) = 𝐸) |
202 | 196, 201 | mpdan 684 |
. 2
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸 ↾s (Base‘𝐹)) = 𝐸) |
203 | 2, 202 | eqtr2d 2779 |
1
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) |