Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diclspsn Structured version   Visualization version   GIF version

Theorem diclspsn 38362
 Description: The value of isomorphism C is spanned by vector 𝐹. Part of proof of Lemma N of [Crawley] p. 121 line 29. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
Hypotheses
Ref Expression
diclspsn.l = (le‘𝐾)
diclspsn.a 𝐴 = (Atoms‘𝐾)
diclspsn.h 𝐻 = (LHyp‘𝐾)
diclspsn.p 𝑃 = ((oc‘𝐾)‘𝑊)
diclspsn.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
diclspsn.i 𝐼 = ((DIsoC‘𝐾)‘𝑊)
diclspsn.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
diclspsn.n 𝑁 = (LSpan‘𝑈)
diclspsn.f 𝐹 = (𝑓𝑇 (𝑓𝑃) = 𝑄)
Assertion
Ref Expression
diclspsn (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐼𝑄) = (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}))
Distinct variable groups:   ,𝑓   𝑃,𝑓   𝐴,𝑓   𝑓,𝐻   𝑇,𝑓   𝑓,𝐾   𝑄,𝑓   𝑓,𝑊
Allowed substitution hints:   𝑈(𝑓)   𝐹(𝑓)   𝐼(𝑓)   𝑁(𝑓)

Proof of Theorem diclspsn
Dummy variables 𝑔 𝑠 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rab 3134 . . 3 {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)} = {𝑣 ∣ (𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))}
2 relopab 5668 . . . . 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 2820 . . . . . . 7 ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
9 diclspsn.i . . . . . . 7 𝐼 = ((DIsoC‘𝐾)‘𝑊)
10 diclspsn.f . . . . . . 7 𝐹 = (𝑓𝑇 (𝑓𝑃) = 𝑄)
113, 4, 5, 6, 7, 8, 9, 10dicval2 38347 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐼𝑄) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 = (𝑧𝐹) ∧ 𝑧 ∈ ((TEndo‘𝐾)‘𝑊))})
1211releqd 5625 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (Rel (𝐼𝑄) ↔ Rel {⟨𝑦, 𝑧⟩ ∣ (𝑦 = (𝑧𝐹) ∧ 𝑧 ∈ ((TEndo‘𝐾)‘𝑊))}))
132, 12mpbiri 260 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → Rel (𝐼𝑄))
14 ssrab2 4031 . . . . . 6 {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)} ⊆ (𝑇 × ((TEndo‘𝐾)‘𝑊))
15 relxp 5545 . . . . . 6 Rel (𝑇 × ((TEndo‘𝐾)‘𝑊))
16 relss 5628 . . . . . 6 ({𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)} ⊆ (𝑇 × ((TEndo‘𝐾)‘𝑊)) → (Rel (𝑇 × ((TEndo‘𝐾)‘𝑊)) → Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)}))
1714, 15, 16mp2 9 . . . . 5 Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)}
1817a1i 11 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
19 id 22 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)))
20 vex 3473 . . . . . . 7 𝑔 ∈ V
21 vex 3473 . . . . . . 7 𝑠 ∈ V
223, 4, 5, 6, 7, 8, 9, 10, 20, 21dicopelval2 38349 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (⟨𝑔, 𝑠⟩ ∈ (𝐼𝑄) ↔ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))))
23 simprl 769 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑔 = (𝑠𝐹))
24 simpll 765 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
25 simprr 771 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))
26 simpl 485 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
273, 4, 5, 6lhpocnel2 37187 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
2827adantr 483 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
29 simpr 487 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
303, 4, 5, 7, 10ltrniotacl 37747 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → 𝐹𝑇)
3126, 28, 29, 30syl3anc 1367 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → 𝐹𝑇)
3231adantr 483 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝐹𝑇)
335, 7, 8tendocl 37935 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝐹𝑇) → (𝑠𝐹) ∈ 𝑇)
3424, 25, 32, 33syl3anc 1367 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑠𝐹) ∈ 𝑇)
3523, 34eqeltrd 2911 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑔𝑇)
3635, 25, 233jca 1124 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹)))
37 simpr3 1192 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹))) → 𝑔 = (𝑠𝐹))
38 simpr2 1191 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹))) → 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))
3937, 38jca 514 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹))) → (𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)))
4036, 39impbida 799 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ((𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹))))
41 diclspsn.u . . . . . . . . . . . . . 14 𝑈 = ((DVecH‘𝐾)‘𝑊)
42 eqid 2820 . . . . . . . . . . . . . 14 (Scalar‘𝑈) = (Scalar‘𝑈)
43 eqid 2820 . . . . . . . . . . . . . 14 (Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈))
445, 8, 41, 42, 43dvhbase 38251 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊))
4544adantr 483 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊))
4645rexeqdv 3396 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)))
47 simpll 765 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
48 simpr 487 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊))
4931adantr 483 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → 𝐹𝑇)
505, 7, 8tendoidcl 37937 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))
5150ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))
52 eqid 2820 . . . . . . . . . . . . . . . . . 18 ( ·𝑠𝑈) = ( ·𝑠𝑈)
535, 7, 8, 41, 52dvhopvsca 38270 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝐹𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) = ⟨(𝑥𝐹), (𝑥 ∘ ( I ↾ 𝑇))⟩)
5447, 48, 49, 51, 53syl13anc 1368 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) = ⟨(𝑥𝐹), (𝑥 ∘ ( I ↾ 𝑇))⟩)
5554eqeq2d 2831 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ ⟨𝑔, 𝑠⟩ = ⟨(𝑥𝐹), (𝑥 ∘ ( I ↾ 𝑇))⟩))
5620, 21opth 5340 . . . . . . . . . . . . . . 15 (⟨𝑔, 𝑠⟩ = ⟨(𝑥𝐹), (𝑥 ∘ ( I ↾ 𝑇))⟩ ↔ (𝑔 = (𝑥𝐹) ∧ 𝑠 = (𝑥 ∘ ( I ↾ 𝑇))))
5755, 56syl6bb 289 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ (𝑔 = (𝑥𝐹) ∧ 𝑠 = (𝑥 ∘ ( I ↾ 𝑇)))))
585, 7, 8tendo1mulr 37939 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ ( I ↾ 𝑇)) = 𝑥)
5958adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ ( I ↾ 𝑇)) = 𝑥)
6059eqeq2d 2831 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑠 = (𝑥 ∘ ( I ↾ 𝑇)) ↔ 𝑠 = 𝑥))
61 equcom 2025 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑥𝑥 = 𝑠)
6260, 61syl6bb 289 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑠 = (𝑥 ∘ ( I ↾ 𝑇)) ↔ 𝑥 = 𝑠))
6362anbi2d 630 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → ((𝑔 = (𝑥𝐹) ∧ 𝑠 = (𝑥 ∘ ( I ↾ 𝑇))) ↔ (𝑔 = (𝑥𝐹) ∧ 𝑥 = 𝑠)))
6457, 63bitrd 281 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ (𝑔 = (𝑥𝐹) ∧ 𝑥 = 𝑠)))
65 ancom 463 . . . . . . . . . . . . 13 ((𝑔 = (𝑥𝐹) ∧ 𝑥 = 𝑠) ↔ (𝑥 = 𝑠𝑔 = (𝑥𝐹)))
6664, 65syl6bb 289 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ (𝑥 = 𝑠𝑔 = (𝑥𝐹))))
6766rexbidva 3281 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹))))
6846, 67bitrd 281 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹))))
69683anbi3d 1438 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ((𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)) ↔ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹)))))
70 fveq1 6641 . . . . . . . . . . . . . 14 (𝑥 = 𝑠 → (𝑥𝐹) = (𝑠𝐹))
7170eqeq2d 2831 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (𝑔 = (𝑥𝐹) ↔ 𝑔 = (𝑠𝐹)))
7271ceqsrexv 3625 . . . . . . . . . . . 12 (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) → (∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹)) ↔ 𝑔 = (𝑠𝐹)))
7372pm5.32i 577 . . . . . . . . . . 11 ((𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹))) ↔ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹)))
7473anbi2i 624 . . . . . . . . . 10 ((𝑔𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹)))) ↔ (𝑔𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹))))
75 3anass 1091 . . . . . . . . . 10 ((𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹))) ↔ (𝑔𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹)))))
76 3anass 1091 . . . . . . . . . 10 ((𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹)) ↔ (𝑔𝑇 ∧ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹))))
7774, 75, 763bitr4i 305 . . . . . . . . 9 ((𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ ((TEndo‘𝐾)‘𝑊)(𝑥 = 𝑠𝑔 = (𝑥𝐹))) ↔ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹)))
7869, 77syl6rbb 290 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ((𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑔 = (𝑠𝐹)) ↔ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))))
7940, 78bitrd 281 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ((𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))))
80 eqeq1 2824 . . . . . . . . . . 11 (𝑣 = ⟨𝑔, 𝑠⟩ → (𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ ⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)))
8180rexbidv 3282 . . . . . . . . . 10 (𝑣 = ⟨𝑔, 𝑠⟩ → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)))
8281rabxp 5572 . . . . . . . . 9 {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)} = {⟨𝑔, 𝑠⟩ ∣ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))}
8382eleq2i 2902 . . . . . . . 8 (⟨𝑔, 𝑠⟩ ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)} ↔ ⟨𝑔, 𝑠⟩ ∈ {⟨𝑔, 𝑠⟩ ∣ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))})
84 opabidw 5384 . . . . . . . 8 (⟨𝑔, 𝑠⟩ ∈ {⟨𝑔, 𝑠⟩ ∣ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))} ↔ (𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)))
8583, 84bitr2i 278 . . . . . . 7 ((𝑔𝑇𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))⟨𝑔, 𝑠⟩ = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)) ↔ ⟨𝑔, 𝑠⟩ ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
8679, 85syl6bb 289 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ((𝑔 = (𝑠𝐹) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ ⟨𝑔, 𝑠⟩ ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)}))
8722, 86bitrd 281 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (⟨𝑔, 𝑠⟩ ∈ (𝐼𝑄) ↔ ⟨𝑔, 𝑠⟩ ∈ {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)}))
8887eqrelrdv2 5640 . . . 4 (((Rel (𝐼𝑄) ∧ Rel {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)}) ∧ ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊))) → (𝐼𝑄) = {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
8913, 18, 19, 88syl21anc 835 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐼𝑄) = {𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
90 simpll 765 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
9145eleq2d 2896 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑥 ∈ (Base‘(Scalar‘𝑈)) ↔ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)))
9291biimpa 479 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊))
9350adantr 483 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))
94 opelxpi 5564 . . . . . . . . . 10 ((𝐹𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) → ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))
9531, 93, 94syl2anc 586 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))
9695adantr 483 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))
975, 7, 8, 41, 52dvhvscacl 38271 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))) → (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))
9890, 92, 96, 97syl12anc 834 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)))
99 eleq1a 2906 . . . . . . 7 ((𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) → (𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) → 𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))))
10098, 99syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑈))) → (𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) → 𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))))
101100rexlimdva 3269 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) → 𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊))))
102101pm4.71rd 565 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩) ↔ (𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))))
103102abbidv 2884 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)} = {𝑣 ∣ (𝑣 ∈ (𝑇 × ((TEndo‘𝐾)‘𝑊)) ∧ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩))})
1041, 89, 1033eqtr4a 2881 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐼𝑄) = {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
1055, 41, 26dvhlmod 38278 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → 𝑈 ∈ LMod)
106 eqid 2820 . . . . 5 (Base‘𝑈) = (Base‘𝑈)
1075, 7, 8, 41, 106dvhelvbasei 38256 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊))) → ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (Base‘𝑈))
10826, 31, 93, 107syl12anc 834 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (Base‘𝑈))
109 diclspsn.n . . . 4 𝑁 = (LSpan‘𝑈)
11042, 43, 106, 52, 109lspsn 19746 . . 3 ((𝑈 ∈ LMod ∧ ⟨𝐹, ( I ↾ 𝑇)⟩ ∈ (Base‘𝑈)) → (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}) = {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
111105, 108, 110syl2anc 586 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}) = {𝑣 ∣ ∃𝑥 ∈ (Base‘(Scalar‘𝑈))𝑣 = (𝑥( ·𝑠𝑈)⟨𝐹, ( I ↾ 𝑇)⟩)})
112104, 111eqtr4d 2858 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐼𝑄) = (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  {cab 2798  ∃wrex 3126  {crab 3129   ⊆ wss 3909  {csn 4539  ⟨cop 4545   class class class wbr 5038  {copab 5100   I cid 5431   × cxp 5525   ↾ cres 5529   ∘ ccom 5531  Rel wrel 5532  ‘cfv 6327  ℩crio 7086  (class class class)co 7129  Basecbs 16458  Scalarcsca 16543   ·𝑠 cvsca 16544  lecple 16547  occoc 16548  LModclmod 19606  LSpanclspn 19715  Atomscatm 36431  HLchlt 36518  LHypclh 37152  LTrncltrn 37269  TEndoctendo 37920  DVecHcdvh 38246  DIsoCcdic 38340 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5162  ax-sep 5175  ax-nul 5182  ax-pow 5238  ax-pr 5302  ax-un 7435  ax-cnex 10567  ax-resscn 10568  ax-1cn 10569  ax-icn 10570  ax-addcl 10571  ax-addrcl 10572  ax-mulcl 10573  ax-mulrcl 10574  ax-mulcom 10575  ax-addass 10576  ax-mulass 10577  ax-distr 10578  ax-i2m1 10579  ax-1ne0 10580  ax-1rid 10581  ax-rnegex 10582  ax-rrecex 10583  ax-cnre 10584  ax-pre-lttri 10585  ax-pre-lttrn 10586  ax-pre-ltadd 10587  ax-pre-mulgt0 10588  ax-riotaBAD 36121 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3472  df-sbc 3749  df-csb 3857  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4811  df-int 4849  df-iun 4893  df-iin 4894  df-br 5039  df-opab 5101  df-mpt 5119  df-tr 5145  df-id 5432  df-eprel 5437  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-riota 7087  df-ov 7132  df-oprab 7133  df-mpo 7134  df-om 7555  df-1st 7663  df-2nd 7664  df-tpos 7866  df-undef 7913  df-wrecs 7921  df-recs 7982  df-rdg 8020  df-1o 8076  df-oadd 8080  df-er 8263  df-map 8382  df-en 8484  df-dom 8485  df-sdom 8486  df-fin 8487  df-pnf 10651  df-mnf 10652  df-xr 10653  df-ltxr 10654  df-le 10655  df-sub 10846  df-neg 10847  df-nn 11613  df-2 11675  df-3 11676  df-4 11677  df-5 11678  df-6 11679  df-n0 11873  df-z 11957  df-uz 12219  df-fz 12873  df-struct 16460  df-ndx 16461  df-slot 16462  df-base 16464  df-sets 16465  df-ress 16466  df-plusg 16553  df-mulr 16554  df-sca 16556  df-vsca 16557  df-0g 16690  df-proset 17513  df-poset 17531  df-plt 17543  df-lub 17559  df-glb 17560  df-join 17561  df-meet 17562  df-p0 17624  df-p1 17625  df-lat 17631  df-clat 17693  df-mgm 17827  df-sgrp 17876  df-mnd 17887  df-grp 18081  df-minusg 18082  df-sbg 18083  df-mgp 19215  df-ur 19227  df-ring 19274  df-oppr 19348  df-dvdsr 19366  df-unit 19367  df-invr 19397  df-dvr 19408  df-drng 19476  df-lmod 19608  df-lss 19676  df-lsp 19716  df-lvec 19847  df-oposet 36344  df-ol 36346  df-oml 36347  df-covers 36434  df-ats 36435  df-atl 36466  df-cvlat 36490  df-hlat 36519  df-llines 36666  df-lplanes 36667  df-lvols 36668  df-lines 36669  df-psubsp 36671  df-pmap 36672  df-padd 36964  df-lhyp 37156  df-laut 37157  df-ldil 37272  df-ltrn 37273  df-trl 37327  df-tendo 37923  df-edring 37925  df-dvech 38247  df-dic 38341 This theorem is referenced by:  cdlemn5pre  38368  dih1dimc  38410
 Copyright terms: Public domain W3C validator