Step | Hyp | Ref
| Expression |
1 | | eqlkr3.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | eqlkr3.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
3 | | eqlkr3.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑊) |
4 | | eqlkr3.r |
. . . . 5
⊢ 𝑅 = (Base‘𝑆) |
5 | | eqlkr3.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
6 | | eqlkr3.f |
. . . . 5
⊢ 𝐹 = (LFnl‘𝑊) |
7 | 3, 4, 5, 6 | lflf 33368 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶𝑅) |
8 | 1, 2, 7 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝐺:𝑉⟶𝑅) |
9 | | ffn 5958 |
. . 3
⊢ (𝐺:𝑉⟶𝑅 → 𝐺 Fn 𝑉) |
10 | 8, 9 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 Fn 𝑉) |
11 | | eqlkr3.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ 𝐹) |
12 | 3, 4, 5, 6 | lflf 33368 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹) → 𝐻:𝑉⟶𝑅) |
13 | 1, 11, 12 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝐻:𝑉⟶𝑅) |
14 | | ffn 5958 |
. . 3
⊢ (𝐻:𝑉⟶𝑅 → 𝐻 Fn 𝑉) |
15 | 13, 14 | syl 17 |
. 2
⊢ (𝜑 → 𝐻 Fn 𝑉) |
16 | | eqlkr3.e |
. . . . . . 7
⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻)) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝑆) = (.r‘𝑆) |
18 | | eqlkr3.k |
. . . . . . . 8
⊢ 𝐾 = (LKer‘𝑊) |
19 | 3, 4, 17, 5, 6, 18 | eqlkr 33404 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐾‘𝐺) = (𝐾‘𝐻)) → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟)) |
20 | 1, 2, 11, 16, 19 | syl121anc 1323 |
. . . . . 6
⊢ (𝜑 → ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟)) |
21 | | eqlkr3.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
22 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑋 ∈ 𝑉) |
23 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝐻‘𝑥) = (𝐻‘𝑋)) |
24 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋)) |
25 | 24 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → ((𝐺‘𝑥)(.r‘𝑆)𝑟) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) |
26 | 23, 25 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) ↔ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟))) |
27 | 26 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) → (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟))) |
28 | 22, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) → (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟))) |
29 | | eqlkr3.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺‘𝑋) = (𝐻‘𝑋)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐺‘𝑋) = (𝐻‘𝑋)) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → (𝐺‘𝑋) = (𝐻‘𝑋)) |
32 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) |
33 | 31, 32 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → ((𝐺‘𝑋)(.r‘𝑆)𝑟) = (𝐺‘𝑋)) |
34 | 33 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)((𝐺‘𝑋)(.r‘𝑆)𝑟)) = (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋))) |
35 | 3 | lvecdrng 18926 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ LVec → 𝑆 ∈
DivRing) |
36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆 ∈ DivRing) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑆 ∈ DivRing) |
38 | 3, 4, 5, 6 | lflcl 33369 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → (𝐺‘𝑋) ∈ 𝑅) |
39 | 1, 2, 21, 38 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝑅) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐺‘𝑋) ∈ 𝑅) |
41 | | eqlkr3.n |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (𝐺‘𝑋) ≠ 0 ) |
43 | | eqlkr3.o |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑆) |
44 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (1r‘𝑆) |
45 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(invr‘𝑆) = (invr‘𝑆) |
46 | 4, 43, 17, 44, 45 | drnginvrl 18589 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝑅 ∧ (𝐺‘𝑋) ≠ 0 ) →
(((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋)) = (1r‘𝑆)) |
47 | 37, 40, 42, 46 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋)) = (1r‘𝑆)) |
48 | 47 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → ((((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋))(.r‘𝑆)𝑟) = ((1r‘𝑆)(.r‘𝑆)𝑟)) |
49 | | lveclmod 18927 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
50 | 1, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑊 ∈ LMod) |
51 | 3 | lmodring 18694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → 𝑆 ∈ Ring) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ Ring) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑆 ∈ Ring) |
54 | 4, 43, 45 | drnginvrcl 18587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ DivRing ∧ (𝐺‘𝑋) ∈ 𝑅 ∧ (𝐺‘𝑋) ≠ 0 ) →
((invr‘𝑆)‘(𝐺‘𝑋)) ∈ 𝑅) |
55 | 37, 40, 42, 54 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → ((invr‘𝑆)‘(𝐺‘𝑋)) ∈ 𝑅) |
56 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅) |
57 | 4, 17 | ringass 18387 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Ring ∧
(((invr‘𝑆)‘(𝐺‘𝑋)) ∈ 𝑅 ∧ (𝐺‘𝑋) ∈ 𝑅 ∧ 𝑟 ∈ 𝑅)) → ((((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋))(.r‘𝑆)𝑟) = (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)((𝐺‘𝑋)(.r‘𝑆)𝑟))) |
58 | 53, 55, 40, 56, 57 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → ((((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋))(.r‘𝑆)𝑟) = (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)((𝐺‘𝑋)(.r‘𝑆)𝑟))) |
59 | 4, 17, 44 | ringlidm 18394 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Ring ∧ 𝑟 ∈ 𝑅) → ((1r‘𝑆)(.r‘𝑆)𝑟) = 𝑟) |
60 | 53, 56, 59 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → ((1r‘𝑆)(.r‘𝑆)𝑟) = 𝑟) |
61 | 48, 58, 60 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)((𝐺‘𝑋)(.r‘𝑆)𝑟)) = 𝑟) |
62 | 61 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)((𝐺‘𝑋)(.r‘𝑆)𝑟)) = 𝑟) |
63 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → (((invr‘𝑆)‘(𝐺‘𝑋))(.r‘𝑆)(𝐺‘𝑋)) = (1r‘𝑆)) |
64 | 34, 62, 63 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ 𝑅) ∧ (𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟)) → 𝑟 = (1r‘𝑆)) |
65 | 64 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → ((𝐻‘𝑋) = ((𝐺‘𝑋)(.r‘𝑆)𝑟) → 𝑟 = (1r‘𝑆))) |
66 | 28, 65 | syld 46 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) → 𝑟 = (1r‘𝑆))) |
67 | 66 | ancrd 575 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ 𝑅) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) → (𝑟 = (1r‘𝑆) ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟)))) |
68 | 67 | reximdva 3000 |
. . . . . 6
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) → ∃𝑟 ∈ 𝑅 (𝑟 = (1r‘𝑆) ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟)))) |
69 | 20, 68 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑟 ∈ 𝑅 (𝑟 = (1r‘𝑆) ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟))) |
70 | 4, 44 | ringidcl 18391 |
. . . . . . 7
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝑅) |
71 | 52, 70 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑆) ∈ 𝑅) |
72 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑟 = (1r‘𝑆) → ((𝐺‘𝑥)(.r‘𝑆)𝑟) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆))) |
73 | 72 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑟 = (1r‘𝑆) → ((𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆)))) |
74 | 73 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑟 = (1r‘𝑆) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆)))) |
75 | 74 | ceqsrexv 3306 |
. . . . . 6
⊢
((1r‘𝑆) ∈ 𝑅 → (∃𝑟 ∈ 𝑅 (𝑟 = (1r‘𝑆) ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟)) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆)))) |
76 | 71, 75 | syl 17 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 (𝑟 = (1r‘𝑆) ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)𝑟)) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆)))) |
77 | 69, 76 | mpbid 221 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆))) |
78 | 77 | r19.21bi 2916 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆))) |
79 | 50 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod) |
80 | 79, 51 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑆 ∈ Ring) |
81 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec) |
82 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹) |
83 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
84 | 3, 4, 5, 6 | lflcl 33369 |
. . . . 5
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝑅) |
85 | 81, 82, 83, 84 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝑅) |
86 | 4, 17, 44 | ringridm 18395 |
. . . 4
⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝑅) → ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆)) = (𝐺‘𝑥)) |
87 | 80, 85, 86 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(.r‘𝑆)(1r‘𝑆)) = (𝐺‘𝑥)) |
88 | 78, 87 | eqtr2d 2645 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐻‘𝑥)) |
89 | 10, 15, 88 | eqfnfvd 6222 |
1
⊢ (𝜑 → 𝐺 = 𝐻) |