Metamath Proof Explorer

Theorem baerlem5a

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. First equation of part (5) in Baer p. 46. (Contributed by NM, 10-Apr-2015)

Ref Expression
Hypotheses baerlem3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
baerlem3.m ⊢ − = ( -g ‘ 𝑊 )
baerlem3.o ⊢ 0 = ( 0g ‘ 𝑊 )
baerlem3.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
baerlem3.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
baerlem3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
baerlem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
baerlem3.c ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
baerlem3.d ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
baerlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
baerlem3.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
baerlem5a.p ⊢ + = ( +g ‘ 𝑊 )
Assertion baerlem5a ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − 𝑍 ) } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) )

Proof

Step Hyp Ref Expression
1 baerlem3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 baerlem3.m ⊢ − = ( -g ‘ 𝑊 )
3 baerlem3.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 baerlem3.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 baerlem3.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6 baerlem3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 baerlem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 baerlem3.c ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
9 baerlem3.d ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
10 baerlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
11 baerlem3.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
12 baerlem5a.p ⊢ + = ( +g ‘ 𝑊 )
13 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
15 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
16 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
17 eqid ⊢ ( -g ‘ ( Scalar ‘ 𝑊 ) ) = ( -g ‘ ( Scalar ‘ 𝑊 ) )
18 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
19 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 baerlem5alem2 ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − 𝑍 ) } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ) )