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

Theorem mapdordlem2 39249
 Description: Lemma for mapdord 39250. Ordering property of projectivity 𝑀. TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the 𝑇 hypothesis. (Contributed by NM, 27-Jan-2015.)
Hypotheses
Ref Expression
mapdord.h 𝐻 = (LHyp‘𝐾)
mapdord.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdord.s 𝑆 = (LSubSp‘𝑈)
mapdord.m 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdord.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
mapdord.x (𝜑𝑋𝑆)
mapdord.y (𝜑𝑌𝑆)
mapdord.o 𝑂 = ((ocH‘𝐾)‘𝑊)
mapdord.a 𝐴 = (LSAtoms‘𝑈)
mapdord.f 𝐹 = (LFnl‘𝑈)
mapdord.c 𝐽 = (LSHyp‘𝑈)
mapdord.l 𝐿 = (LKer‘𝑈)
mapdord.t 𝑇 = {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) ∈ 𝐽}
mapdord.q 𝐶 = {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)}
Assertion
Ref Expression
mapdordlem2 (𝜑 → ((𝑀𝑋) ⊆ (𝑀𝑌) ↔ 𝑋𝑌))
Distinct variable groups:   𝑔,𝐾   𝑈,𝑔   𝑔,𝑊   𝑔,𝐹   𝑔,𝐽   𝑔,𝐿   𝑔,𝑂
Allowed substitution hints:   𝜑(𝑔)   𝐴(𝑔)   𝐶(𝑔)   𝑆(𝑔)   𝑇(𝑔)   𝐻(𝑔)   𝑀(𝑔)   𝑋(𝑔)   𝑌(𝑔)

Proof of Theorem mapdordlem2
Dummy variables 𝑓 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mapdord.h . . . 4 𝐻 = (LHyp‘𝐾)
2 mapdord.u . . . 4 𝑈 = ((DVecH‘𝐾)‘𝑊)
3 mapdord.s . . . 4 𝑆 = (LSubSp‘𝑈)
4 mapdord.f . . . 4 𝐹 = (LFnl‘𝑈)
5 mapdord.l . . . 4 𝐿 = (LKer‘𝑈)
6 mapdord.o . . . 4 𝑂 = ((ocH‘𝐾)‘𝑊)
7 mapdord.m . . . 4 𝑀 = ((mapd‘𝐾)‘𝑊)
8 mapdord.k . . . 4 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
9 mapdord.x . . . 4 (𝜑𝑋𝑆)
10 mapdord.q . . . 4 𝐶 = {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) = (𝐿𝑔)}
111, 2, 3, 4, 5, 6, 7, 8, 9, 10mapdvalc 39241 . . 3 (𝜑 → (𝑀𝑋) = {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋})
12 mapdord.y . . . 4 (𝜑𝑌𝑆)
131, 2, 3, 4, 5, 6, 7, 8, 12, 10mapdvalc 39241 . . 3 (𝜑 → (𝑀𝑌) = {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌})
1411, 13sseq12d 3928 . 2 (𝜑 → ((𝑀𝑋) ⊆ (𝑀𝑌) ↔ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌}))
15 ss2rab 3978 . . . . 5 ({𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌} ↔ ∀𝑓𝐶 ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌))
16 eqid 2759 . . . . . . . . 9 (Base‘𝑈) = (Base‘𝑈)
17 mapdord.c . . . . . . . . 9 𝐽 = (LSHyp‘𝑈)
18 mapdord.t . . . . . . . . 9 𝑇 = {𝑔𝐹 ∣ (𝑂‘(𝑂‘(𝐿𝑔))) ∈ 𝐽}
191, 6, 2, 16, 17, 4, 5, 18, 10, 8mapdordlem1a 39246 . . . . . . . 8 (𝜑 → (𝑓𝑇 ↔ (𝑓𝐶 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)))
20 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑓𝐶 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)) → 𝑓𝐶)
21 idd 24 . . . . . . . . . 10 ((𝜑 ∧ (𝑓𝐶 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)) → (((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌) → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
2220, 21embantd 59 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐶 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)) → ((𝑓𝐶 → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)) → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
2322ex 416 . . . . . . . 8 (𝜑 → ((𝑓𝐶 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽) → ((𝑓𝐶 → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)) → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌))))
2419, 23sylbid 243 . . . . . . 7 (𝜑 → (𝑓𝑇 → ((𝑓𝐶 → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)) → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌))))
2524com23 86 . . . . . 6 (𝜑 → ((𝑓𝐶 → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)) → (𝑓𝑇 → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌))))
2625ralimdv2 3108 . . . . 5 (𝜑 → (∀𝑓𝐶 ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌) → ∀𝑓𝑇 ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
2715, 26syl5bi 245 . . . 4 (𝜑 → ({𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌} → ∀𝑓𝑇 ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
28 mapdord.a . . . . . 6 𝐴 = (LSAtoms‘𝑈)
291, 2, 8dvhlmod 38722 . . . . . 6 (𝜑𝑈 ∈ LMod)
303, 28, 29, 9, 12lssatle 36627 . . . . 5 (𝜑 → (𝑋𝑌 ↔ ∀𝑝𝐴 (𝑝𝑋𝑝𝑌)))
3118mapdordlem1 39248 . . . . . . . . . . 11 (𝑓𝑇 ↔ (𝑓𝐹 ∧ (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽))
3231simprbi 500 . . . . . . . . . 10 (𝑓𝑇 → (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)
3332adantl 485 . . . . . . . . 9 ((𝜑𝑓𝑇) → (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)
348adantr 484 . . . . . . . . . 10 ((𝜑𝑓𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
3531simplbi 501 . . . . . . . . . . 11 (𝑓𝑇𝑓𝐹)
3635adantl 485 . . . . . . . . . 10 ((𝜑𝑓𝑇) → 𝑓𝐹)
371, 6, 2, 4, 17, 5, 34, 36dochlkr 38997 . . . . . . . . 9 ((𝜑𝑓𝑇) → ((𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽 ↔ ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝐿𝑓) ∈ 𝐽)))
3833, 37mpbid 235 . . . . . . . 8 ((𝜑𝑓𝑇) → ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ∧ (𝐿𝑓) ∈ 𝐽))
3938simpld 498 . . . . . . 7 ((𝜑𝑓𝑇) → (𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓))
4038simprd 499 . . . . . . . 8 ((𝜑𝑓𝑇) → (𝐿𝑓) ∈ 𝐽)
411, 6, 2, 28, 17, 34, 40dochshpsat 39066 . . . . . . 7 ((𝜑𝑓𝑇) → ((𝑂‘(𝑂‘(𝐿𝑓))) = (𝐿𝑓) ↔ (𝑂‘(𝐿𝑓)) ∈ 𝐴))
4239, 41mpbid 235 . . . . . 6 ((𝜑𝑓𝑇) → (𝑂‘(𝐿𝑓)) ∈ 𝐴)
431, 2, 8dvhlvec 38721 . . . . . . . . . . 11 (𝜑𝑈 ∈ LVec)
4443adantr 484 . . . . . . . . . 10 ((𝜑𝑝𝐴) → 𝑈 ∈ LVec)
458adantr 484 . . . . . . . . . . 11 ((𝜑𝑝𝐴) → (𝐾 ∈ HL ∧ 𝑊𝐻))
46 simpr 488 . . . . . . . . . . 11 ((𝜑𝑝𝐴) → 𝑝𝐴)
471, 2, 6, 28, 17, 45, 46dochsatshp 39063 . . . . . . . . . 10 ((𝜑𝑝𝐴) → (𝑂𝑝) ∈ 𝐽)
4817, 4, 5lshpkrex 36730 . . . . . . . . . 10 ((𝑈 ∈ LVec ∧ (𝑂𝑝) ∈ 𝐽) → ∃𝑓𝐹 (𝐿𝑓) = (𝑂𝑝))
4944, 47, 48syl2anc 587 . . . . . . . . 9 ((𝜑𝑝𝐴) → ∃𝑓𝐹 (𝐿𝑓) = (𝑂𝑝))
50 df-rex 3077 . . . . . . . . 9 (∃𝑓𝐹 (𝐿𝑓) = (𝑂𝑝) ↔ ∃𝑓(𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝)))
5149, 50sylib 221 . . . . . . . 8 ((𝜑𝑝𝐴) → ∃𝑓(𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝)))
52 simprl 770 . . . . . . . . . . . 12 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → 𝑓𝐹)
53 simprr 772 . . . . . . . . . . . . . . . 16 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝐿𝑓) = (𝑂𝑝))
5453fveq2d 6668 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂‘(𝐿𝑓)) = (𝑂‘(𝑂𝑝)))
5554fveq2d 6668 . . . . . . . . . . . . . 14 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂‘(𝑂‘(𝐿𝑓))) = (𝑂‘(𝑂‘(𝑂𝑝))))
5629adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝𝐴) → 𝑈 ∈ LMod)
5716, 28, 56, 46lsatssv 36610 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝𝐴) → 𝑝 ⊆ (Base‘𝑈))
58 eqid 2759 . . . . . . . . . . . . . . . . . 18 ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
591, 58, 2, 16, 6dochcl 38965 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝 ⊆ (Base‘𝑈)) → (𝑂𝑝) ∈ ran ((DIsoH‘𝐾)‘𝑊))
6045, 57, 59syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑝𝐴) → (𝑂𝑝) ∈ ran ((DIsoH‘𝐾)‘𝑊))
611, 58, 6dochoc 38979 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑂𝑝) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑂‘(𝑂‘(𝑂𝑝))) = (𝑂𝑝))
6245, 60, 61syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑝𝐴) → (𝑂‘(𝑂‘(𝑂𝑝))) = (𝑂𝑝))
6362adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂‘(𝑂‘(𝑂𝑝))) = (𝑂𝑝))
6455, 63eqtrd 2794 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂‘(𝑂‘(𝐿𝑓))) = (𝑂𝑝))
6547adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂𝑝) ∈ 𝐽)
6664, 65eqeltrd 2853 . . . . . . . . . . . 12 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂‘(𝑂‘(𝐿𝑓))) ∈ 𝐽)
6752, 66, 31sylanbrc 586 . . . . . . . . . . 11 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → 𝑓𝑇)
681, 2, 58, 28dih1dimat 38942 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝𝐴) → 𝑝 ∈ ran ((DIsoH‘𝐾)‘𝑊))
6945, 46, 68syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑝𝐴) → 𝑝 ∈ ran ((DIsoH‘𝐾)‘𝑊))
701, 58, 6dochoc 38979 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑂‘(𝑂𝑝)) = 𝑝)
7145, 69, 70syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑝𝐴) → (𝑂‘(𝑂𝑝)) = 𝑝)
7271adantr 484 . . . . . . . . . . . 12 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑂‘(𝑂𝑝)) = 𝑝)
7354, 72eqtr2d 2795 . . . . . . . . . . 11 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → 𝑝 = (𝑂‘(𝐿𝑓)))
7467, 73jca 515 . . . . . . . . . 10 (((𝜑𝑝𝐴) ∧ (𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝))) → (𝑓𝑇𝑝 = (𝑂‘(𝐿𝑓))))
7574ex 416 . . . . . . . . 9 ((𝜑𝑝𝐴) → ((𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝)) → (𝑓𝑇𝑝 = (𝑂‘(𝐿𝑓)))))
7675eximdv 1919 . . . . . . . 8 ((𝜑𝑝𝐴) → (∃𝑓(𝑓𝐹 ∧ (𝐿𝑓) = (𝑂𝑝)) → ∃𝑓(𝑓𝑇𝑝 = (𝑂‘(𝐿𝑓)))))
7751, 76mpd 15 . . . . . . 7 ((𝜑𝑝𝐴) → ∃𝑓(𝑓𝑇𝑝 = (𝑂‘(𝐿𝑓))))
78 df-rex 3077 . . . . . . 7 (∃𝑓𝑇 𝑝 = (𝑂‘(𝐿𝑓)) ↔ ∃𝑓(𝑓𝑇𝑝 = (𝑂‘(𝐿𝑓))))
7977, 78sylibr 237 . . . . . 6 ((𝜑𝑝𝐴) → ∃𝑓𝑇 𝑝 = (𝑂‘(𝐿𝑓)))
80 sseq1 3920 . . . . . . . 8 (𝑝 = (𝑂‘(𝐿𝑓)) → (𝑝𝑋 ↔ (𝑂‘(𝐿𝑓)) ⊆ 𝑋))
81 sseq1 3920 . . . . . . . 8 (𝑝 = (𝑂‘(𝐿𝑓)) → (𝑝𝑌 ↔ (𝑂‘(𝐿𝑓)) ⊆ 𝑌))
8280, 81imbi12d 348 . . . . . . 7 (𝑝 = (𝑂‘(𝐿𝑓)) → ((𝑝𝑋𝑝𝑌) ↔ ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
8382adantl 485 . . . . . 6 ((𝜑𝑝 = (𝑂‘(𝐿𝑓))) → ((𝑝𝑋𝑝𝑌) ↔ ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
8442, 79, 83ralxfrd 5282 . . . . 5 (𝜑 → (∀𝑝𝐴 (𝑝𝑋𝑝𝑌) ↔ ∀𝑓𝑇 ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)))
8530, 84bitr2d 283 . . . 4 (𝜑 → (∀𝑓𝑇 ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌) ↔ 𝑋𝑌))
8627, 85sylibd 242 . . 3 (𝜑 → ({𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌} → 𝑋𝑌))
87 simplr 768 . . . . . 6 (((𝜑𝑋𝑌) ∧ 𝑓𝐶) → 𝑋𝑌)
88 sstr 3903 . . . . . . . 8 (((𝑂‘(𝐿𝑓)) ⊆ 𝑋𝑋𝑌) → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)
8988ancoms 462 . . . . . . 7 ((𝑋𝑌 ∧ (𝑂‘(𝐿𝑓)) ⊆ 𝑋) → (𝑂‘(𝐿𝑓)) ⊆ 𝑌)
9089a1i 11 . . . . . 6 (((𝜑𝑋𝑌) ∧ 𝑓𝐶) → ((𝑋𝑌 ∧ (𝑂‘(𝐿𝑓)) ⊆ 𝑋) → (𝑂‘(𝐿𝑓)) ⊆ 𝑌))
9187, 90mpand 694 . . . . 5 (((𝜑𝑋𝑌) ∧ 𝑓𝐶) → ((𝑂‘(𝐿𝑓)) ⊆ 𝑋 → (𝑂‘(𝐿𝑓)) ⊆ 𝑌))
9291ss2rabdv 3983 . . . 4 ((𝜑𝑋𝑌) → {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌})
9392ex 416 . . 3 (𝜑 → (𝑋𝑌 → {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌}))
9486, 93impbid 215 . 2 (𝜑 → ({𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑋} ⊆ {𝑓𝐶 ∣ (𝑂‘(𝐿𝑓)) ⊆ 𝑌} ↔ 𝑋𝑌))
9514, 94bitrd 282 1 (𝜑 → ((𝑀𝑋) ⊆ (𝑀𝑌) ↔ 𝑋𝑌))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∀wral 3071  ∃wrex 3072  {crab 3075   ⊆ wss 3861  ran crn 5530  ‘cfv 6341  Basecbs 16556  LModclmod 19717  LSubSpclss 19786  LVecclvec 19957  LSAtomsclsa 36586  LSHypclsh 36587  LFnlclfn 36669  LKerclk 36697  HLchlt 36962  LHypclh 37596  DVecHcdvh 38690  DIsoHcdih 38840  ocHcoch 38959  mapdcmpd 39236 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-riotaBAD 36565 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-iin 4890  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-tpos 7909  df-undef 7956  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-1o 8119  df-er 8306  df-map 8425  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-nn 11689  df-2 11751  df-3 11752  df-4 11753  df-5 11754  df-6 11755  df-n0 11949  df-z 12035  df-uz 12297  df-fz 12954  df-struct 16558  df-ndx 16559  df-slot 16560  df-base 16562  df-sets 16563  df-ress 16564  df-plusg 16651  df-mulr 16652  df-sca 16654  df-vsca 16655  df-0g 16788  df-proset 17619  df-poset 17637  df-plt 17649  df-lub 17665  df-glb 17666  df-join 17667  df-meet 17668  df-p0 17730  df-p1 17731  df-lat 17737  df-clat 17799  df-mgm 17933  df-sgrp 17982  df-mnd 17993  df-submnd 18038  df-grp 18187  df-minusg 18188  df-sbg 18189  df-subg 18358  df-cntz 18529  df-lsm 18843  df-cmn 18990  df-abl 18991  df-mgp 19323  df-ur 19335  df-ring 19382  df-oppr 19459  df-dvdsr 19477  df-unit 19478  df-invr 19508  df-dvr 19519  df-drng 19587  df-lmod 19719  df-lss 19787  df-lsp 19827  df-lvec 19958  df-lsatoms 36588  df-lshyp 36589  df-lfl 36670  df-lkr 36698  df-oposet 36788  df-ol 36790  df-oml 36791  df-covers 36878  df-ats 36879  df-atl 36910  df-cvlat 36934  df-hlat 36963  df-llines 37110  df-lplanes 37111  df-lvols 37112  df-lines 37113  df-psubsp 37115  df-pmap 37116  df-padd 37408  df-lhyp 37600  df-laut 37601  df-ldil 37716  df-ltrn 37717  df-trl 37771  df-tgrp 38355  df-tendo 38367  df-edring 38369  df-dveca 38615  df-disoa 38641  df-dvech 38691  df-dib 38751  df-dic 38785  df-dih 38841  df-doch 38960  df-djh 39007  df-mapd 39237 This theorem is referenced by:  mapdord  39250
 Copyright terms: Public domain W3C validator