Proof of Theorem lclkrlem2m
| Step | Hyp | Ref
| Expression |
| 1 | | lclkrlem2m.b |
. . 3
⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) |
| 2 | | lclkrlem2m.w |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ LVec) |
| 3 | | lveclmod 21105 |
. . . . . 6
⊢ (𝑈 ∈ LVec → 𝑈 ∈ LMod) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ LMod) |
| 5 | | lmodgrp 20865 |
. . . . 5
⊢ (𝑈 ∈ LMod → 𝑈 ∈ Grp) |
| 6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Grp) |
| 7 | | lclkrlem2m.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 8 | | lclkrlem2m.s |
. . . . . . . 8
⊢ 𝑆 = (Scalar‘𝑈) |
| 9 | 8 | lmodring 20866 |
. . . . . . 7
⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring) |
| 10 | 4, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ Ring) |
| 11 | | lclkrlem2m.f |
. . . . . . . 8
⊢ 𝐹 = (LFnl‘𝑈) |
| 12 | | lclkrlem2m.d |
. . . . . . . 8
⊢ 𝐷 = (LDual‘𝑈) |
| 13 | | lclkrlem2m.p |
. . . . . . . 8
⊢ + =
(+g‘𝐷) |
| 14 | | lclkrlem2m.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ 𝐹) |
| 15 | | lclkrlem2m.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
| 16 | 11, 12, 13, 4, 14, 15 | ldualvaddcl 39131 |
. . . . . . 7
⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 18 | | lclkrlem2m.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑈) |
| 19 | 8, 17, 18, 11 | lflcl 39065 |
. . . . . . 7
⊢ ((𝑈 ∈ LVec ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆)) |
| 20 | 2, 16, 7, 19 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆)) |
| 21 | 8 | lvecdrng 21104 |
. . . . . . . 8
⊢ (𝑈 ∈ LVec → 𝑆 ∈
DivRing) |
| 22 | 2, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ DivRing) |
| 23 | | lclkrlem2m.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 24 | 8, 17, 18, 11 | lflcl 39065 |
. . . . . . . 8
⊢ ((𝑈 ∈ LVec ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆)) |
| 25 | 2, 16, 23, 24 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆)) |
| 26 | | lclkrlem2m.n |
. . . . . . 7
⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) |
| 27 | | lclkrlem2m.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑆) |
| 28 | | lclkrlem2m.i |
. . . . . . . 8
⊢ 𝐼 = (invr‘𝑆) |
| 29 | 17, 27, 28 | drnginvrcl 20753 |
. . . . . . 7
⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) |
| 30 | 22, 25, 26, 29 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) |
| 31 | | lclkrlem2m.q |
. . . . . . 7
⊢ × =
(.r‘𝑆) |
| 32 | 17, 31 | ringcl 20247 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆)) |
| 33 | 10, 20, 30, 32 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆)) |
| 34 | | lclkrlem2m.t |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑈) |
| 35 | 18, 8, 34, 17 | lmodvscl 20876 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉) |
| 36 | 4, 33, 23, 35 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉) |
| 37 | | lclkrlem2m.m |
. . . . 5
⊢ − =
(-g‘𝑈) |
| 38 | 18, 37 | grpsubcl 19038 |
. . . 4
⊢ ((𝑈 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉) → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) ∈ 𝑉) |
| 39 | 6, 7, 36, 38 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) ∈ 𝑉) |
| 40 | 1, 39 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 41 | 1 | fveq2i 6909 |
. . 3
⊢ ((𝐸 + 𝐺)‘𝐵) = ((𝐸 + 𝐺)‘(𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))) |
| 42 | | eqid 2737 |
. . . . . 6
⊢
(-g‘𝑆) = (-g‘𝑆) |
| 43 | 8, 42, 18, 37, 11 | lflsub 39068 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ (𝑋 ∈ 𝑉 ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)) → ((𝐸 + 𝐺)‘(𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))) = (((𝐸 + 𝐺)‘𝑋)(-g‘𝑆)((𝐸 + 𝐺)‘((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))) |
| 44 | 4, 16, 7, 36, 43 | syl112anc 1376 |
. . . 4
⊢ (𝜑 → ((𝐸 + 𝐺)‘(𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))) = (((𝐸 + 𝐺)‘𝑋)(-g‘𝑆)((𝐸 + 𝐺)‘((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))) |
| 45 | 8, 17, 31, 18, 34, 11 | lflmul 39069 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉)) → ((𝐸 + 𝐺)‘((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) × ((𝐸 + 𝐺)‘𝑌))) |
| 46 | 4, 16, 33, 23, 45 | syl112anc 1376 |
. . . . . 6
⊢ (𝜑 → ((𝐸 + 𝐺)‘((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) × ((𝐸 + 𝐺)‘𝑌))) |
| 47 | 17, 31 | ringass 20250 |
. . . . . . . 8
⊢ ((𝑆 ∈ Ring ∧ (((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) × ((𝐸 + 𝐺)‘𝑌)) = (((𝐸 + 𝐺)‘𝑋) × ((𝐼‘((𝐸 + 𝐺)‘𝑌)) × ((𝐸 + 𝐺)‘𝑌)))) |
| 48 | 10, 20, 30, 25, 47 | syl13anc 1374 |
. . . . . . 7
⊢ (𝜑 → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) × ((𝐸 + 𝐺)‘𝑌)) = (((𝐸 + 𝐺)‘𝑋) × ((𝐼‘((𝐸 + 𝐺)‘𝑌)) × ((𝐸 + 𝐺)‘𝑌)))) |
| 49 | | eqid 2737 |
. . . . . . . . . 10
⊢
(1r‘𝑆) = (1r‘𝑆) |
| 50 | 17, 27, 31, 49, 28 | drnginvrl 20756 |
. . . . . . . . 9
⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → ((𝐼‘((𝐸 + 𝐺)‘𝑌)) × ((𝐸 + 𝐺)‘𝑌)) = (1r‘𝑆)) |
| 51 | 22, 25, 26, 50 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼‘((𝐸 + 𝐺)‘𝑌)) × ((𝐸 + 𝐺)‘𝑌)) = (1r‘𝑆)) |
| 52 | 51 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × ((𝐼‘((𝐸 + 𝐺)‘𝑌)) × ((𝐸 + 𝐺)‘𝑌))) = (((𝐸 + 𝐺)‘𝑋) ×
(1r‘𝑆))) |
| 53 | 48, 52 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) × ((𝐸 + 𝐺)‘𝑌)) = (((𝐸 + 𝐺)‘𝑋) ×
(1r‘𝑆))) |
| 54 | 17, 31, 49 | ringridm 20267 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) ×
(1r‘𝑆)) =
((𝐸 + 𝐺)‘𝑋)) |
| 55 | 10, 20, 54 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) ×
(1r‘𝑆)) =
((𝐸 + 𝐺)‘𝑋)) |
| 56 | 46, 53, 55 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ((𝐸 + 𝐺)‘((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = ((𝐸 + 𝐺)‘𝑋)) |
| 57 | 56 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋)(-g‘𝑆)((𝐸 + 𝐺)‘((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))) = (((𝐸 + 𝐺)‘𝑋)(-g‘𝑆)((𝐸 + 𝐺)‘𝑋))) |
| 58 | | ringgrp 20235 |
. . . . . 6
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
| 59 | 10, 58 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Grp) |
| 60 | 17, 27, 42 | grpsubid 19042 |
. . . . 5
⊢ ((𝑆 ∈ Grp ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋)(-g‘𝑆)((𝐸 + 𝐺)‘𝑋)) = 0 ) |
| 61 | 59, 20, 60 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋)(-g‘𝑆)((𝐸 + 𝐺)‘𝑋)) = 0 ) |
| 62 | 44, 57, 61 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → ((𝐸 + 𝐺)‘(𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))) = 0 ) |
| 63 | 41, 62 | eqtrid 2789 |
. 2
⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 0 ) |
| 64 | 40, 63 | jca 511 |
1
⊢ (𝜑 → (𝐵 ∈ 𝑉 ∧ ((𝐸 + 𝐺)‘𝐵) = 0 )) |