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 |
10
|
eldifad |
⊢ ( 𝜑 → 𝑌 ∈ 𝑉 ) |
14 |
11
|
eldifad |
⊢ ( 𝜑 → 𝑍 ∈ 𝑉 ) |
15 |
|
eqid |
⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 ) |
16 |
1 12 15 2
|
grpsubval |
⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) |
17 |
13 14 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) |
18 |
17
|
sneqd |
⊢ ( 𝜑 → { ( 𝑌 − 𝑍 ) } = { ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) } ) |
19 |
18
|
fveq2d |
⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 − 𝑍 ) } ) = ( 𝑁 ‘ { ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) } ) ) |
20 |
|
lveclmod |
⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod ) |
21 |
6 20
|
syl |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
22 |
1 15
|
lmodvnegcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ 𝑉 ) |
23 |
21 14 22
|
syl2anc |
⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ 𝑉 ) |
24 |
|
eqid |
⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) |
25 |
1 24 5 21 13 14
|
lspprcl |
⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ) |
26 |
3 24 21 25 7 8
|
lssneln0 |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ) |
27 |
1 5 6 7 13 14 8
|
lspindpi |
⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ) ) |
28 |
27
|
simpld |
⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) |
29 |
1 3 5 6 26 13 28
|
lspsnne1 |
⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) |
30 |
9
|
necomd |
⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) |
31 |
1 3 5 6 11 13 30
|
lspsnne1 |
⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) ) |
32 |
1 5 6 7 14 13 31 8
|
lspexchn2 |
⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) |
33 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
34 |
21 33
|
syl |
⊢ ( 𝜑 → 𝑊 ∈ Grp ) |
35 |
34
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑊 ∈ Grp ) |
36 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑍 ∈ 𝑉 ) |
37 |
1 15
|
grpinvinv |
⊢ ( ( 𝑊 ∈ Grp ∧ 𝑍 ∈ 𝑉 ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) = 𝑍 ) |
38 |
35 36 37
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) = 𝑍 ) |
39 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑊 ∈ LMod ) |
40 |
1 24 5 21 13 7
|
lspprcl |
⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) |
41 |
40
|
adantr |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) |
42 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) |
43 |
24 15
|
lssvnegcl |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) |
44 |
39 41 42 43
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) |
45 |
38 44
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) |
46 |
32 45
|
mtand |
⊢ ( 𝜑 → ¬ ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ) |
47 |
1 5 6 23 7 13 29 46
|
lspexchn2 |
⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) ) |
48 |
1 15 5
|
lspsnneg |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) = ( 𝑁 ‘ { 𝑍 } ) ) |
49 |
21 14 48
|
syl2anc |
⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) = ( 𝑁 ‘ { 𝑍 } ) ) |
50 |
9 49
|
neeqtrrd |
⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) ) |
51 |
1 3 15
|
grpinvnzcl |
⊢ ( ( 𝑊 ∈ Grp ∧ 𝑍 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑉 ∖ { 0 } ) ) |
52 |
34 11 51
|
syl2anc |
⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ∈ ( 𝑉 ∖ { 0 } ) ) |
53 |
1 2 3 4 5 6 7 47 50 10 52 12
|
baerlem5b |
⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) |
54 |
49
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) ) = ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ) |
55 |
17
|
eqcomd |
⊢ ( 𝜑 → ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) = ( 𝑌 − 𝑍 ) ) |
56 |
55
|
oveq2d |
⊢ ( 𝜑 → ( 𝑋 − ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) = ( 𝑋 − ( 𝑌 − 𝑍 ) ) ) |
57 |
56
|
sneqd |
⊢ ( 𝜑 → { ( 𝑋 − ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) } = { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) |
58 |
57
|
fveq2d |
⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) } ) = ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) ) |
59 |
58
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) |
60 |
54 59
|
ineq12d |
⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + ( ( invg ‘ 𝑊 ) ‘ 𝑍 ) ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) |
61 |
19 53 60
|
3eqtrd |
⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 − 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 − 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ) |