Step |
Hyp |
Ref |
Expression |
1 |
|
dvalvec.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dvalvec.v |
⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
eqid |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
eqid |
⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
1 3 4 5 2
|
dvaset |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 = ( { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠 ‘ 𝑓 ) ) 〉 } ) ) |
7 |
|
eqid |
⊢ ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
1 3 7
|
tgrpset |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) = { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 } ) |
9 |
1 7
|
tgrpabl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 ) ∈ Abel ) |
10 |
8 9
|
eqeltrrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 } ∈ Abel ) |
11 |
|
fvex |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V |
12 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 } = { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 } |
13 |
12
|
grpbase |
⊢ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 } ) ) |
14 |
|
eqid |
⊢ ( { 〈 ( 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 |
⊢ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ ( { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠 ‘ 𝑓 ) ) 〉 } ) ) ) |
16 |
13 15
|
eqtr3d |
⊢ ( ( ( 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 |
⊢ ( 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
|
mpoex |
⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V |
19 |
12
|
grpplusg |
⊢ ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 } ) ) |
20 |
14
|
lmodplusg |
⊢ ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ∈ V → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( +g ‘ ( { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠 ‘ 𝑓 ) ) 〉 } ) ) ) |
21 |
19 20
|
eqtr3d |
⊢ ( ( 𝑓 ∈ ( ( 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 |
⊢ ( +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 |
⊢ ( { 〈 ( 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 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( { 〈 ( Base ‘ ndx ) , ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) , 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑠 ‘ 𝑓 ) ) 〉 } ) ∈ Abel ) |
25 |
6 24
|
eqeltrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ Abel ) |