Step |
Hyp |
Ref |
Expression |
1 |
|
dvhfvadd.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dvhfvadd.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
dvhfvadd.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
dvhfvadd.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
dvhfvadd.f |
⊢ 𝐷 = ( Scalar ‘ 𝑈 ) |
6 |
|
dvhfvadd.p |
⊢ ⨣ = ( +g ‘ 𝐷 ) |
7 |
|
dvhfvadd.a |
⊢ ✚ = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) 〉 ) |
8 |
|
dvhfvadd.s |
⊢ + = ( +g ‘ 𝑈 ) |
9 |
|
eqid |
⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) |
10 |
1 2 3 9 4
|
dvhset |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 = ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) ) |
11 |
10
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝑈 ) = ( +g ‘ ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) ) ) |
12 |
1 9 4 5
|
dvhsca |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) |
13 |
12
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝐷 ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
14 |
6 13
|
syl5eq |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
15 |
14
|
oveqd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) = ( ( 2nd ‘ 𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd ‘ 𝑔 ) ) ) |
16 |
15
|
3ad2ant1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) = ( ( 2nd ‘ 𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd ‘ 𝑔 ) ) ) |
17 |
|
xp2nd |
⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) |
18 |
|
xp2nd |
⊢ ( 𝑔 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑔 ) ∈ 𝐸 ) |
19 |
17 18
|
anim12i |
⊢ ( ( 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd ‘ 𝑓 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝑔 ) ∈ 𝐸 ) ) |
20 |
|
eqid |
⊢ ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) |
21 |
1 2 3 9 20
|
erngplus |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2nd ‘ 𝑓 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝑔 ) ∈ 𝐸 ) ) → ( ( 2nd ‘ 𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd ‘ 𝑔 ) ) = ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ) |
22 |
19 21
|
sylan2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd ‘ 𝑔 ) ) = ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ) |
23 |
22
|
3impb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd ‘ 𝑓 ) ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) ( 2nd ‘ 𝑔 ) ) = ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ) |
24 |
16 23
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) = ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) ) |
25 |
24
|
opeq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) 〉 = 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) |
26 |
25
|
mpoeq3dva |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) 〉 ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) ) |
27 |
2
|
fvexi |
⊢ 𝑇 ∈ V |
28 |
3
|
fvexi |
⊢ 𝐸 ∈ V |
29 |
27 28
|
xpex |
⊢ ( 𝑇 × 𝐸 ) ∈ V |
30 |
29 29
|
mpoex |
⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) ∈ V |
31 |
|
eqid |
⊢ ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) = ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) |
32 |
31
|
lmodplusg |
⊢ ( ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) ∈ V → ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) = ( +g ‘ ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) ) ) |
33 |
30 32
|
ax-mp |
⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) = ( +g ‘ ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) ) |
34 |
26 33
|
eqtr2di |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ ( { 〈 ( Base ‘ ndx ) , ( 𝑇 × 𝐸 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ℎ ∈ 𝑇 ↦ ( ( ( 2nd ‘ 𝑓 ) ‘ ℎ ) ∘ ( ( 2nd ‘ 𝑔 ) ‘ ℎ ) ) ) 〉 ) 〉 , 〈 ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) 〉 } ∪ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) 〉 } ) ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) 〉 ) ) |
35 |
11 34
|
eqtrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝑈 ) = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) ⨣ ( 2nd ‘ 𝑔 ) ) 〉 ) ) |
36 |
35 8 7
|
3eqtr4g |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ✚ ) |