Metamath Proof Explorer


Theorem baerlem3

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Part (3) in Baer p. 45. TODO fix ref. (Contributed by NM, 9-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 } ) )
Assertion baerlem3 ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ) ) )

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 eqid ( +g𝑊 ) = ( +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 baerlem3lem2 ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ) ) )