Step | Hyp | Ref
| Expression |
1 | | dvalvec.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | eqid 2610 |
. . 3
⊢
((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) |
3 | | eqid 2610 |
. . 3
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) |
4 | | eqid 2610 |
. . 3
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
5 | | dvalvec.v |
. . 3
⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) |
6 | 1, 2, 3, 4, 5 | dvaset 35311 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 = ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉})) |
7 | | eqid 2610 |
. . . . 5
⊢
((TGrp‘𝐾)‘𝑊) = ((TGrp‘𝐾)‘𝑊) |
8 | 1, 2, 7 | tgrpset 35051 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((TGrp‘𝐾)‘𝑊) = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) |
9 | 1, 7 | tgrpabl 35057 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((TGrp‘𝐾)‘𝑊) ∈ Abel) |
10 | 8, 9 | eqeltrrd 2689 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉} ∈ Abel) |
11 | | fvex 6113 |
. . . . 5
⊢
((LTrn‘𝐾)‘𝑊) ∈ V |
12 | | eqid 2610 |
. . . . . . 7
⊢
{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉} = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉} |
13 | 12 | grpbase 15816 |
. . . . . 6
⊢
(((LTrn‘𝐾)‘𝑊) ∈ V → ((LTrn‘𝐾)‘𝑊) = (Base‘{〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉})) |
14 | | eqid 2610 |
. . . . . . 7
⊢
({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}) = ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}) |
15 | 14 | lmodbase 15841 |
. . . . . 6
⊢
(((LTrn‘𝐾)‘𝑊) ∈ V → ((LTrn‘𝐾)‘𝑊) = (Base‘({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}))) |
16 | 13, 15 | eqtr3d 2646 |
. . . . 5
⊢
(((LTrn‘𝐾)‘𝑊) ∈ V →
(Base‘{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) =
(Base‘({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}))) |
17 | 11, 16 | ax-mp 5 |
. . . 4
⊢
(Base‘{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) =
(Base‘({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉})) |
18 | 11, 11 | mpt2ex 7136 |
. . . . 5
⊢ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) ∈ V |
19 | 12 | grpplusg 15817 |
. . . . . 6
⊢ ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) ∈ V → (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) =
(+g‘{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉})) |
20 | 14 | lmodplusg 15842 |
. . . . . 6
⊢ ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) ∈ V → (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) =
(+g‘({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}))) |
21 | 19, 20 | eqtr3d 2646 |
. . . . 5
⊢ ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) ∈ V →
(+g‘{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) =
(+g‘({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}))) |
22 | 18, 21 | ax-mp 5 |
. . . 4
⊢
(+g‘{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) =
(+g‘({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉})) |
23 | 17, 22 | ablprop 18027 |
. . 3
⊢
({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉} ∈ Abel ↔
({〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}) ∈ Abel) |
24 | 10, 23 | sylib 207 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ({〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉, 〈(Scalar‘ndx),
((EDRing‘𝐾)‘𝑊)〉} ∪ {〈(
·𝑠 ‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑠‘𝑓))〉}) ∈ Abel) |
25 | 6, 24 | eqeltrd 2688 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Abel) |