Step |
Hyp |
Ref |
Expression |
1 |
|
lfl1dim.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
lfl1dim.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
3 |
|
lfl1dim.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
4 |
|
lfl1dim.l |
⊢ 𝐿 = ( LKer ‘ 𝑊 ) |
5 |
|
lfl1dim.k |
⊢ 𝐾 = ( Base ‘ 𝐷 ) |
6 |
|
lfl1dim.t |
⊢ · = ( .r ‘ 𝐷 ) |
7 |
|
lfl1dim.w |
⊢ ( 𝜑 → 𝑊 ∈ LVec ) |
8 |
|
lfl1dim.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝐹 ) |
9 |
|
df-rab |
⊢ { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∣ ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) } |
10 |
|
lveclmod |
⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod ) |
11 |
7 10
|
syl |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
12 |
|
eqid |
⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 ) |
13 |
2 5 12
|
lmod0cl |
⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝐷 ) ∈ 𝐾 ) |
14 |
11 13
|
syl |
⊢ ( 𝜑 → ( 0g ‘ 𝐷 ) ∈ 𝐾 ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 0g ‘ 𝐷 ) ∈ 𝐾 ) |
16 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
17 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑊 ∈ LMod ) |
18 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝐺 ∈ 𝐹 ) |
19 |
1 2 3 5 6 12 17 18
|
lfl0sc |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
20 |
16 19
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
21 |
|
sneq |
⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → { 𝑘 } = { ( 0g ‘ 𝐷 ) } ) |
22 |
21
|
xpeq2d |
⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → ( 𝑉 × { 𝑘 } ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
23 |
22
|
oveq2d |
⊢ ( 𝑘 = ( 0g ‘ 𝐷 ) → ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
24 |
23
|
rspceeqv |
⊢ ( ( ( 0g ‘ 𝐷 ) ∈ 𝐾 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) |
25 |
15 20 24
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) |
26 |
25
|
a1d |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
27 |
14
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 0g ‘ 𝐷 ) ∈ 𝐾 ) |
28 |
11
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LMod ) |
29 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 ) |
30 |
1 3 4 28 29
|
lkrssv |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 ) |
31 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝑊 ∈ LMod ) |
32 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → 𝐺 ∈ 𝐹 ) |
33 |
2 12 1 3 4
|
lkr0f |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
34 |
31 32 33
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
35 |
34
|
biimpar |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 ) |
36 |
35
|
sseq1d |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) ) ) |
37 |
36
|
biimpa |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑉 ⊆ ( 𝐿 ‘ 𝑔 ) ) |
38 |
30 37
|
eqssd |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝑔 ) = 𝑉 ) |
39 |
2 12 1 3 4
|
lkr0f |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
40 |
28 29 39
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
41 |
38 40
|
mpbid |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
42 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 ) |
43 |
1 2 3 5 6 12 28 42
|
lfl0sc |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
44 |
41 43
|
eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) |
45 |
27 44 24
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) |
46 |
45
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
47 |
|
eqid |
⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 ) |
48 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑊 ∈ LVec ) |
49 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝐺 ∈ 𝐹 ) |
50 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
51 |
1 2 12 47 3 4
|
lkrshp |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) ) |
52 |
48 49 50 51
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑊 ) ) |
53 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑔 ∈ 𝐹 ) |
54 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) |
55 |
1 2 12 47 3 4
|
lkrshp |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) ) |
56 |
48 53 54 55
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ( LSHyp ‘ 𝑊 ) ) |
57 |
47 48 52 56
|
lshpcmp |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) ) |
58 |
7
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑊 ∈ LVec ) |
59 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝐺 ∈ 𝐹 ) |
60 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → 𝑔 ∈ 𝐹 ) |
61 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) |
62 |
2 5 6 1 3 4
|
eqlkr2 |
⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) |
63 |
58 59 60 61 62
|
syl121anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) |
64 |
63
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
65 |
57 64
|
sylbid |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝑔 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ 𝐷 ) } ) ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
66 |
26 46 65
|
pm2.61da2ne |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) → ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
67 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑊 ∈ LVec ) |
68 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 ) |
69 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ 𝐾 ) |
70 |
1 2 5 6 3 4 67 68 69
|
lkrscss |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
71 |
70
|
ex |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) ) |
72 |
|
fveq2 |
⊢ ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝑔 ) = ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
73 |
72
|
sseq2d |
⊢ ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) ) |
74 |
73
|
biimprcd |
⊢ ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ) |
75 |
71 74
|
syl6 |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑘 ∈ 𝐾 → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ) ) |
76 |
75
|
rexlimdv |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ) |
77 |
66 76
|
impbid |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
78 |
77
|
pm5.32da |
⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ↔ ( 𝑔 ∈ 𝐹 ∧ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) ) |
79 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝑊 ∈ LMod ) |
80 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐺 ∈ 𝐹 ) |
81 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ 𝐾 ) |
82 |
1 2 5 6 3 79 80 81
|
lflvscl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ∈ 𝐹 ) |
83 |
|
eleq1a |
⊢ ( ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ∈ 𝐹 → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → 𝑔 ∈ 𝐹 ) ) |
84 |
82 83
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) → 𝑔 ∈ 𝐹 ) ) |
85 |
84
|
pm4.71rd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ↔ ( 𝑔 ∈ 𝐹 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) ) |
86 |
85
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ↔ ∃ 𝑘 ∈ 𝐾 ( 𝑔 ∈ 𝐹 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) ) |
87 |
|
r19.42v |
⊢ ( ∃ 𝑘 ∈ 𝐾 ( 𝑔 ∈ 𝐹 ∧ 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ↔ ( 𝑔 ∈ 𝐹 ∧ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
88 |
86 87
|
bitr2di |
⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐹 ∧ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
89 |
78 88
|
bitrd |
⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) ↔ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) ) ) |
90 |
89
|
abbidv |
⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 ∈ 𝐹 ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) } ) |
91 |
9 90
|
syl5eq |
⊢ ( 𝜑 → { 𝑔 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑔 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝐾 𝑔 = ( 𝐺 ∘f · ( 𝑉 × { 𝑘 } ) ) } ) |