Step | Hyp | Ref
| Expression |
1 | | dvalvec.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | eqid 2733 |
. . 3
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
3 | | eqid 2733 |
. . 3
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
4 | | eqid 2733 |
. . 3
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
5 | | dvalvec.v |
. . 3
β’ π = ((DVecAβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | dvaset 39518 |
. 2
β’ ((πΎ β HL β§ π β π») β π = ({β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π βπ))β©})) |
7 | | eqid 2733 |
. . . . 5
β’
((TGrpβπΎ)βπ) = ((TGrpβπΎ)βπ) |
8 | 1, 2, 7 | tgrpset 39258 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ((TGrpβπΎ)βπ) = {β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©}) |
9 | 1, 7 | tgrpabl 39264 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ((TGrpβπΎ)βπ) β Abel) |
10 | 8, 9 | eqeltrrd 2835 |
. . 3
β’ ((πΎ β HL β§ π β π») β {β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©} β Abel) |
11 | | fvex 6859 |
. . . . 5
β’
((LTrnβπΎ)βπ) β V |
12 | | eqid 2733 |
. . . . . . 7
β’
{β¨(Baseβndx), ((LTrnβπΎ)βπ)β©, β¨(+gβndx),
(π β
((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©} = {β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©} |
13 | 12 | grpbase 17175 |
. . . . . 6
β’
(((LTrnβπΎ)βπ) β V β ((LTrnβπΎ)βπ) = (Baseβ{β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©})) |
14 | | eqid 2733 |
. . . . . . 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 17215 |
. . . . . 6
β’
(((LTrnβπΎ)βπ) β V β ((LTrnβπΎ)βπ) = (Baseβ({β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π βπ))β©}))) |
16 | 13, 15 | eqtr3d 2775 |
. . . . 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 | mpoex 8016 |
. . . . 5
β’ (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π)) β V |
19 | 12 | grpplusg 17177 |
. . . . . 6
β’ ((π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π)) β V β (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π)) =
(+gβ{β¨(Baseβndx), ((LTrnβπΎ)βπ)β©, β¨(+gβndx),
(π β
((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©})) |
20 | 14 | lmodplusg 17216 |
. . . . . 6
β’ ((π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π)) β V β (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π)) =
(+gβ({β¨(Baseβndx), ((LTrnβπΎ)βπ)β©, β¨(+gβndx),
(π β
((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π βπ))β©}))) |
21 | 19, 20 | eqtr3d 2775 |
. . . . 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 19583 |
. . 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 217 |
. 2
β’ ((πΎ β HL β§ π β π») β ({β¨(Baseβndx),
((LTrnβπΎ)βπ)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ), π β ((LTrnβπΎ)βπ) β¦ (π βπ))β©}) β Abel) |
25 | 6, 24 | eqeltrd 2834 |
1
β’ ((πΎ β HL β§ π β π») β π β Abel) |