Step |
Hyp |
Ref |
Expression |
1 |
|
lfldi.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lfldi.r |
⊢ 𝑅 = ( Scalar ‘ 𝑊 ) |
3 |
|
lfldi.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
4 |
|
lfldi.p |
⊢ + = ( +g ‘ 𝑅 ) |
5 |
|
lfldi.t |
⊢ · = ( .r ‘ 𝑅 ) |
6 |
|
lfldi.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
7 |
|
lfldi.w |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
8 |
|
lfldi.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐾 ) |
9 |
|
lfldi2.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐾 ) |
10 |
|
lfldi2.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝐹 ) |
11 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
12 |
11
|
a1i |
⊢ ( 𝜑 → 𝑉 ∈ V ) |
13 |
12 8 9
|
ofc12 |
⊢ ( 𝜑 → ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) = ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) |
14 |
13
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) ) |
15 |
1 2 3 4 5 6 7 8 9 10
|
lflvsdi2 |
⊢ ( 𝜑 → ( 𝐺 ∘f · ( ( 𝑉 × { 𝑋 } ) ∘f + ( 𝑉 × { 𝑌 } ) ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺 ∘f · ( 𝑉 × { 𝑌 } ) ) ) ) |
16 |
14 15
|
eqtr3d |
⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝐺 ∘f · ( 𝑉 × { 𝑋 } ) ) ∘f + ( 𝐺 ∘f · ( 𝑉 × { 𝑌 } ) ) ) ) |