Step | Hyp | Ref
| Expression |
1 | | df-rab 3073 |
. . 3
⊢ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} = {𝑣 ∣ (𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))} |
2 | | relopabv 5731 |
. . . . 5
⊢ Rel
{〈𝑦, 𝑧〉 ∣ (𝑦 = (𝑧‘𝐹) ∧ 𝑧 ∈ ((TEndo‘𝐾)‘𝑊))} |
3 | | diclspsn.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
4 | | diclspsn.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | diclspsn.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | diclspsn.p |
. . . . . . 7
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
7 | | diclspsn.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
8 | | eqid 2738 |
. . . . . . 7
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) |
9 | | diclspsn.i |
. . . . . . 7
⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) |
10 | | diclspsn.f |
. . . . . . 7
⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑄) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | dicval2 39193 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {〈𝑦, 𝑧〉 ∣ (𝑦 = (𝑧‘𝐹) ∧ 𝑧 ∈ ((TEndo‘𝐾)‘𝑊))}) |
12 | 11 | releqd 5689 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (Rel (𝐼‘𝑄) ↔ Rel {〈𝑦, 𝑧〉 ∣ (𝑦 = (𝑧‘𝐹) ∧ 𝑧 ∈ ((TEndo‘𝐾)‘𝑊))})) |
13 | 2, 12 | mpbiri 257 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → Rel (𝐼‘𝑄)) |
14 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} ⊆ (𝑇 × ((TEndo‘𝐾)‘𝑊)) |
15 | | relxp 5607 |
. . . . . 6
⊢ Rel
(𝑇 ×
((TEndo‘𝐾)‘𝑊)) |
16 | | relss 5692 |
. . . . . 6
⊢ ({𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} ⊆ (𝑇 × ((TEndo‘𝐾)‘𝑊)) → (Rel (𝑇 × ((TEndo‘𝐾)‘𝑊)) → Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)})) |
17 | 14, 15, 16 | mp2 9 |
. . . . 5
⊢ Rel
{𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} |
18 | 17 | a1i 11 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
19 | | id 22 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) |
20 | | vex 3436 |
. . . . . . 7
⊢ 𝑔 ∈ V |
21 | | vex 3436 |
. . . . . . 7
⊢ 𝑠 ∈ V |
22 | 3, 4, 5, 6, 7, 8, 9, 10, 20, 21 | dicopelval2 39195 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑔, 𝑠〉 ∈ (𝐼‘𝑄) ↔ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)))) |
23 | | simprl 768 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑔 = (𝑠‘𝐹)) |
24 | | simpll 764 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
25 | | simprr 770 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) |
26 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
27 | 3, 4, 5, 6 | lhpocnel2 38033 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
29 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
30 | 3, 4, 5, 7, 10 | ltrniotacl 38593 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
31 | 26, 28, 29, 30 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
32 | 31 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝐹 ∈ 𝑇) |
33 | 5, 7, 8 | tendocl 38781 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇) |
34 | 24, 25, 32, 33 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑠‘𝐹) ∈ 𝑇) |
35 | 23, 34 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑔 ∈ 𝑇) |
36 | 35, 25, 23 | 3jca 1127 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹))) |
37 | | simpr3 1195 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹))) → 𝑔 = (𝑠‘𝐹)) |
38 | | simpr2 1194 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹))) → 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) |
39 | 37, 38 | jca 512 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹))) → (𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) |
40 | 36, 39 | impbida 798 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹)))) |
41 | | diclspsn.u |
. . . . . . . . . . . . . 14
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
42 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
43 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
44 | 5, 8, 41, 42, 43 | dvhbase 39097 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊)) |
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊)) |
46 | 45 | rexeqdv 3349 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))) |
47 | | simpll 764 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
48 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) |
49 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → 𝐹 ∈ 𝑇) |
50 | 5, 7, 8 | tendoidcl 38783 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
51 | 50 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
52 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
53 | 5, 7, 8, 41, 52 | dvhopvsca 39116 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) = 〈(𝑥‘𝐹), (𝑥 ∘ ( I ↾ 𝑇))〉) |
54 | 47, 48, 49, 51, 53 | syl13anc 1371 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) = 〈(𝑥‘𝐹), (𝑥 ∘ ( I ↾ 𝑇))〉) |
55 | 54 | eqeq2d 2749 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ 〈𝑔, 𝑠〉 = 〈(𝑥‘𝐹), (𝑥 ∘ ( I ↾ 𝑇))〉)) |
56 | 20, 21 | opth 5391 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑔, 𝑠〉 = 〈(𝑥‘𝐹), (𝑥 ∘ ( I ↾ 𝑇))〉 ↔ (𝑔 = (𝑥‘𝐹) ∧ 𝑠 = (𝑥 ∘ ( I ↾ 𝑇)))) |
57 | 55, 56 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ (𝑔 = (𝑥‘𝐹) ∧ 𝑠 = (𝑥 ∘ ( I ↾ 𝑇))))) |
58 | 5, 7, 8 | tendo1mulr 38785 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ ( I ↾ 𝑇)) = 𝑥) |
59 | 58 | adantlr 712 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ ( I ↾ 𝑇)) = 𝑥) |
60 | 59 | eqeq2d 2749 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑠 = (𝑥 ∘ ( I ↾ 𝑇)) ↔ 𝑠 = 𝑥)) |
61 | | equcom 2021 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑥 ↔ 𝑥 = 𝑠) |
62 | 60, 61 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑠 = (𝑥 ∘ ( I ↾ 𝑇)) ↔ 𝑥 = 𝑠)) |
63 | 62 | anbi2d 629 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → ((𝑔 = (𝑥‘𝐹) ∧ 𝑠 = (𝑥 ∘ ( I ↾ 𝑇))) ↔ (𝑔 = (𝑥‘𝐹) ∧ 𝑥 = 𝑠))) |
64 | 57, 63 | bitrd 278 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ (𝑔 = (𝑥‘𝐹) ∧ 𝑥 = 𝑠))) |
65 | | ancom 461 |
. . . . . . . . . . . . 13
⊢ ((𝑔 = (𝑥‘𝐹) ∧ 𝑥 = 𝑠) ↔ (𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹))) |
66 | 64, 65 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ (𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹)))) |
67 | 66 | rexbidva 3225 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹)))) |
68 | 46, 67 | bitrd 278 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹)))) |
69 | 68 | 3anbi3d 1441 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)) ↔ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹))))) |
70 | | fveq1 6773 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑠 → (𝑥‘𝐹) = (𝑠‘𝐹)) |
71 | 70 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑠 → (𝑔 = (𝑥‘𝐹) ↔ 𝑔 = (𝑠‘𝐹))) |
72 | 71 | ceqsrexv 3585 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) → (∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹)) ↔ 𝑔 = (𝑠‘𝐹))) |
73 | 72 | pm5.32i 575 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹))) ↔ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹))) |
74 | 73 | anbi2i 623 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹)))) ↔ (𝑔 ∈ 𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹)))) |
75 | | 3anass 1094 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹))) ↔ (𝑔 ∈ 𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹))))) |
76 | | 3anass 1094 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹)) ↔ (𝑔 ∈ 𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹)))) |
77 | 74, 75, 76 | 3bitr4i 303 |
. . . . . . . . 9
⊢ ((𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠 ∧ 𝑔 = (𝑥‘𝐹))) ↔ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹))) |
78 | 69, 77 | bitr2di 288 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠‘𝐹)) ↔ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)))) |
79 | 40, 78 | bitrd 278 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)))) |
80 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑣 = 〈𝑔, 𝑠〉 → (𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ 〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))) |
81 | 80 | rexbidv 3226 |
. . . . . . . . . 10
⊢ (𝑣 = 〈𝑔, 𝑠〉 → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))) |
82 | 81 | rabxp 5635 |
. . . . . . . . 9
⊢ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} = {〈𝑔, 𝑠〉 ∣ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))} |
83 | 82 | eleq2i 2830 |
. . . . . . . 8
⊢
(〈𝑔, 𝑠〉 ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} ↔ 〈𝑔, 𝑠〉 ∈ {〈𝑔, 𝑠〉 ∣ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))}) |
84 | | opabidw 5437 |
. . . . . . . 8
⊢
(〈𝑔, 𝑠〉 ∈ {〈𝑔, 𝑠〉 ∣ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))} ↔ (𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))) |
85 | 83, 84 | bitr2i 275 |
. . . . . . 7
⊢ ((𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))〈𝑔, 𝑠〉 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)) ↔ 〈𝑔, 𝑠〉 ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
86 | 79, 85 | bitrdi 287 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑔 = (𝑠‘𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ 〈𝑔, 𝑠〉 ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)})) |
87 | 22, 86 | bitrd 278 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝑔, 𝑠〉 ∈ (𝐼‘𝑄) ↔ 〈𝑔, 𝑠〉 ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)})) |
88 | 87 | eqrelrdv2 5705 |
. . . 4
⊢ (((Rel
(𝐼‘𝑄) ∧ Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝐼‘𝑄) = {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
89 | 13, 18, 19, 88 | syl21anc 835 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
90 | | simpll 764 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
91 | 45 | eleq2d 2824 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑥 ∈ (Base‘(Scalar‘𝑈)) ↔ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊))) |
92 | 91 | biimpa 477 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) |
93 | 50 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
94 | | opelxpi 5626 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) → 〈𝐹, ( I ↾ 𝑇)〉 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))) |
95 | 31, 93, 94 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 〈𝐹, ( I ↾ 𝑇)〉 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))) |
96 | 95 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → 〈𝐹, ( I ↾ 𝑇)〉 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))) |
97 | 5, 7, 8, 41, 52 | dvhvscacl 39117 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 〈𝐹, ( I ↾ 𝑇)〉 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))) → (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))) |
98 | 90, 92, 96, 97 | syl12anc 834 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))) |
99 | | eleq1a 2834 |
. . . . . . 7
⊢ ((𝑥(
·𝑠 ‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) → (𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) → 𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))) |
100 | 98, 99 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → (𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) → 𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))) |
101 | 100 | rexlimdva 3213 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) → 𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))) |
102 | 101 | pm4.71rd 563 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉) ↔ (𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)))) |
103 | 102 | abbidv 2807 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)} = {𝑣 ∣ (𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉))}) |
104 | 1, 89, 103 | 3eqtr4a 2804 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
105 | 5, 41, 26 | dvhlmod 39124 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝑈 ∈ LMod) |
106 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
107 | 5, 7, 8, 41, 106 | dvhelvbasei 39102 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))) → 〈𝐹, ( I ↾ 𝑇)〉 ∈ (Base‘𝑈)) |
108 | 26, 31, 93, 107 | syl12anc 834 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 〈𝐹, ( I ↾ 𝑇)〉 ∈ (Base‘𝑈)) |
109 | | diclspsn.n |
. . . 4
⊢ 𝑁 = (LSpan‘𝑈) |
110 | 42, 43, 106, 52, 109 | lspsn 20264 |
. . 3
⊢ ((𝑈 ∈ LMod ∧ 〈𝐹, ( I ↾ 𝑇)〉 ∈ (Base‘𝑈)) → (𝑁‘{〈𝐹, ( I ↾ 𝑇)〉}) = {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
111 | 105, 108,
110 | syl2anc 584 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑁‘{〈𝐹, ( I ↾ 𝑇)〉}) = {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠
‘𝑈)〈𝐹, ( I ↾ 𝑇)〉)}) |
112 | 104, 111 | eqtr4d 2781 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = (𝑁‘{〈𝐹, ( I ↾ 𝑇)〉})) |