Step |
Hyp |
Ref |
Expression |
1 |
|
lspextmo.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
2 |
|
lspextmo.k |
⊢ 𝐾 = ( LSpan ‘ 𝑆 ) |
3 |
|
eqtr3 |
⊢ ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) ) |
4 |
|
inss1 |
⊢ ( 𝑔 ∩ ℎ ) ⊆ 𝑔 |
5 |
|
dmss |
⊢ ( ( 𝑔 ∩ ℎ ) ⊆ 𝑔 → dom ( 𝑔 ∩ ℎ ) ⊆ dom 𝑔 ) |
6 |
4 5
|
ax-mp |
⊢ dom ( 𝑔 ∩ ℎ ) ⊆ dom 𝑔 |
7 |
|
eqid |
⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 ) |
8 |
1 7
|
lmhmf |
⊢ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ) |
9 |
8
|
ad2antrl |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ) |
10 |
9
|
ffnd |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → 𝑔 Fn 𝐵 ) |
11 |
10
|
adantrr |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝑔 Fn 𝐵 ) |
12 |
11
|
fndmd |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom 𝑔 = 𝐵 ) |
13 |
6 12
|
sseqtrid |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom ( 𝑔 ∩ ℎ ) ⊆ 𝐵 ) |
14 |
|
simplr |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → ( 𝐾 ‘ 𝑋 ) = 𝐵 ) |
15 |
|
lmhmlmod1 |
⊢ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod ) |
16 |
15
|
adantr |
⊢ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑆 ∈ LMod ) |
17 |
16
|
ad2antrl |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝑆 ∈ LMod ) |
18 |
|
eqid |
⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 ) |
19 |
18
|
lmhmeql |
⊢ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) → dom ( 𝑔 ∩ ℎ ) ∈ ( LSubSp ‘ 𝑆 ) ) |
20 |
19
|
ad2antrl |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom ( 𝑔 ∩ ℎ ) ∈ ( LSubSp ‘ 𝑆 ) ) |
21 |
|
simprr |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) |
22 |
18 2
|
lspssp |
⊢ ( ( 𝑆 ∈ LMod ∧ dom ( 𝑔 ∩ ℎ ) ∈ ( LSubSp ‘ 𝑆 ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) → ( 𝐾 ‘ 𝑋 ) ⊆ dom ( 𝑔 ∩ ℎ ) ) |
23 |
17 20 21 22
|
syl3anc |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → ( 𝐾 ‘ 𝑋 ) ⊆ dom ( 𝑔 ∩ ℎ ) ) |
24 |
14 23
|
eqsstrrd |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝐵 ⊆ dom ( 𝑔 ∩ ℎ ) ) |
25 |
13 24
|
eqssd |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom ( 𝑔 ∩ ℎ ) = 𝐵 ) |
26 |
25
|
expr |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) → dom ( 𝑔 ∩ ℎ ) = 𝐵 ) ) |
27 |
|
simprr |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) |
28 |
1 7
|
lmhmf |
⊢ ( ℎ ∈ ( 𝑆 LMHom 𝑇 ) → ℎ : 𝐵 ⟶ ( Base ‘ 𝑇 ) ) |
29 |
|
ffn |
⊢ ( ℎ : 𝐵 ⟶ ( Base ‘ 𝑇 ) → ℎ Fn 𝐵 ) |
30 |
27 28 29
|
3syl |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ℎ Fn 𝐵 ) |
31 |
|
simpll |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → 𝑋 ⊆ 𝐵 ) |
32 |
|
fnreseql |
⊢ ( ( 𝑔 Fn 𝐵 ∧ ℎ Fn 𝐵 ∧ 𝑋 ⊆ 𝐵 ) → ( ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) |
33 |
10 30 31 32
|
syl3anc |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) |
34 |
|
fneqeql |
⊢ ( ( 𝑔 Fn 𝐵 ∧ ℎ Fn 𝐵 ) → ( 𝑔 = ℎ ↔ dom ( 𝑔 ∩ ℎ ) = 𝐵 ) ) |
35 |
10 30 34
|
syl2anc |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( 𝑔 = ℎ ↔ dom ( 𝑔 ∩ ℎ ) = 𝐵 ) ) |
36 |
26 33 35
|
3imtr4d |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) → 𝑔 = ℎ ) ) |
37 |
3 36
|
syl5 |
⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → 𝑔 = ℎ ) ) |
38 |
37
|
ralrimivva |
⊢ ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) → ∀ 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∀ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → 𝑔 = ℎ ) ) |
39 |
|
reseq1 |
⊢ ( 𝑔 = ℎ → ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) ) |
40 |
39
|
eqeq1d |
⊢ ( 𝑔 = ℎ → ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ↔ ( ℎ ↾ 𝑋 ) = 𝐹 ) ) |
41 |
40
|
rmo4 |
⊢ ( ∃* 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ( 𝑔 ↾ 𝑋 ) = 𝐹 ↔ ∀ 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∀ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → 𝑔 = ℎ ) ) |
42 |
38 41
|
sylibr |
⊢ ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) → ∃* 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ( 𝑔 ↾ 𝑋 ) = 𝐹 ) |