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

Theorem mapdpglem30 36510
 Description: Lemma for mapdpg 36514. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 36509, using lvecindp2 19079) that v = 1 and v = u...". TODO: would it be shorter to have only the 𝑣 = (1r‘𝐴) part and use mapdpglem28.u2 in mapdpglem31 36511? (Contributed by NM, 22-Mar-2015.)
Hypotheses
Ref Expression
mapdpg.h 𝐻 = (LHyp‘𝐾)
mapdpg.m 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdpg.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdpg.v 𝑉 = (Base‘𝑈)
mapdpg.s = (-g𝑈)
mapdpg.z 0 = (0g𝑈)
mapdpg.n 𝑁 = (LSpan‘𝑈)
mapdpg.c 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdpg.f 𝐹 = (Base‘𝐶)
mapdpg.r 𝑅 = (-g𝐶)
mapdpg.j 𝐽 = (LSpan‘𝐶)
mapdpg.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
mapdpg.x (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
mapdpg.y (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
mapdpg.g (𝜑𝐺𝐹)
mapdpg.ne (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
mapdpg.e (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))
mapdpgem25.h1 (𝜑 → (𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅)}))))
mapdpgem25.i1 (𝜑 → (𝑖𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))
mapdpglem26.a 𝐴 = (Scalar‘𝑈)
mapdpglem26.b 𝐵 = (Base‘𝐴)
mapdpglem26.t · = ( ·𝑠𝐶)
mapdpglem26.o 𝑂 = (0g𝐴)
mapdpglem28.ve (𝜑𝑣𝐵)
mapdpglem28.u1 (𝜑 = (𝑢 · 𝑖))
mapdpglem28.u2 (𝜑 → (𝐺𝑅) = (𝑣 · (𝐺𝑅𝑖)))
mapdpglem28.ue (𝜑𝑢𝐵)
Assertion
Ref Expression
mapdpglem30 (𝜑 → (𝑣 = (1r𝐴) ∧ 𝑣 = 𝑢))
Distinct variable groups:   ,𝑖,𝑢,𝑣   𝑢,𝐵,𝑣   𝑢,𝐶,𝑣   𝑢,𝑂,𝑣   𝑢, · ,𝑣   𝑣,𝐺   𝑣,𝑅
Allowed substitution hints:   𝜑(𝑣,𝑢,,𝑖)   𝐴(𝑣,𝑢,,𝑖)   𝐵(,𝑖)   𝐶(,𝑖)   𝑅(𝑢,,𝑖)   · (,𝑖)   𝑈(𝑣,𝑢,,𝑖)   𝐹(𝑣,𝑢,,𝑖)   𝐺(𝑢,,𝑖)   𝐻(𝑣,𝑢,,𝑖)   𝐽(𝑣,𝑢,,𝑖)   𝐾(𝑣,𝑢,,𝑖)   𝑀(𝑣,𝑢,,𝑖)   (𝑣,𝑢,,𝑖)   𝑁(𝑣,𝑢,,𝑖)   𝑂(,𝑖)   𝑉(𝑣,𝑢,,𝑖)   𝑊(𝑣,𝑢,,𝑖)   𝑋(𝑣,𝑢,,𝑖)   𝑌(𝑣,𝑢,,𝑖)   0 (𝑣,𝑢,,𝑖)

Proof of Theorem mapdpglem30
StepHypRef Expression
1 mapdpg.f . . 3 𝐹 = (Base‘𝐶)
2 eqid 2621 . . 3 (+g𝐶) = (+g𝐶)
3 eqid 2621 . . 3 (Scalar‘𝐶) = (Scalar‘𝐶)
4 eqid 2621 . . 3 (Base‘(Scalar‘𝐶)) = (Base‘(Scalar‘𝐶))
5 mapdpglem26.t . . 3 · = ( ·𝑠𝐶)
6 eqid 2621 . . 3 (0g𝐶) = (0g𝐶)
7 mapdpg.j . . 3 𝐽 = (LSpan‘𝐶)
8 mapdpg.h . . . 4 𝐻 = (LHyp‘𝐾)
9 mapdpg.c . . . 4 𝐶 = ((LCDual‘𝐾)‘𝑊)
10 mapdpg.k . . . 4 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
118, 9, 10lcdlvec 36399 . . 3 (𝜑𝐶 ∈ LVec)
12 mapdpg.g . . . 4 (𝜑𝐺𝐹)
13 mapdpg.m . . . . 5 𝑀 = ((mapd‘𝐾)‘𝑊)
14 mapdpg.u . . . . 5 𝑈 = ((DVecH‘𝐾)‘𝑊)
15 mapdpg.v . . . . 5 𝑉 = (Base‘𝑈)
16 mapdpg.s . . . . 5 = (-g𝑈)
17 mapdpg.z . . . . 5 0 = (0g𝑈)
18 mapdpg.n . . . . 5 𝑁 = (LSpan‘𝑈)
19 mapdpg.r . . . . 5 𝑅 = (-g𝐶)
20 mapdpg.x . . . . 5 (𝜑𝑋 ∈ (𝑉 ∖ { 0 }))
21 mapdpg.y . . . . 5 (𝜑𝑌 ∈ (𝑉 ∖ { 0 }))
22 mapdpg.ne . . . . 5 (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
23 mapdpg.e . . . . 5 (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺}))
248, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23mapdpglem30a 36503 . . . 4 (𝜑𝐺 ≠ (0g𝐶))
25 eldifsn 4294 . . . 4 (𝐺 ∈ (𝐹 ∖ {(0g𝐶)}) ↔ (𝐺𝐹𝐺 ≠ (0g𝐶)))
2612, 24, 25sylanbrc 697 . . 3 (𝜑𝐺 ∈ (𝐹 ∖ {(0g𝐶)}))
27 mapdpgem25.i1 . . . . 5 (𝜑 → (𝑖𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅𝑖)}))))
2827simpld 475 . . . 4 (𝜑𝑖𝐹)
29 mapdpgem25.h1 . . . . 5 (𝜑 → (𝐹 ∧ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{}) ∧ (𝑀‘(𝑁‘{(𝑋 𝑌)})) = (𝐽‘{(𝐺𝑅)}))))
308, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27mapdpglem30b 36504 . . . 4 (𝜑𝑖 ≠ (0g𝐶))
31 eldifsn 4294 . . . 4 (𝑖 ∈ (𝐹 ∖ {(0g𝐶)}) ↔ (𝑖𝐹𝑖 ≠ (0g𝐶)))
3228, 30, 31sylanbrc 697 . . 3 (𝜑𝑖 ∈ (𝐹 ∖ {(0g𝐶)}))
33 mapdpglem28.ve . . . 4 (𝜑𝑣𝐵)
34 mapdpglem26.a . . . . 5 𝐴 = (Scalar‘𝑈)
35 mapdpglem26.b . . . . 5 𝐵 = (Base‘𝐴)
368, 14, 34, 35, 9, 3, 4, 10lcdsbase 36408 . . . 4 (𝜑 → (Base‘(Scalar‘𝐶)) = 𝐵)
3733, 36eleqtrrd 2701 . . 3 (𝜑𝑣 ∈ (Base‘(Scalar‘𝐶)))
388, 14, 10dvhlmod 35918 . . . . . 6 (𝜑𝑈 ∈ LMod)
3934lmodring 18811 . . . . . 6 (𝑈 ∈ LMod → 𝐴 ∈ Ring)
4038, 39syl 17 . . . . 5 (𝜑𝐴 ∈ Ring)
41 ringgrp 18492 . . . . . . 7 (𝐴 ∈ Ring → 𝐴 ∈ Grp)
4240, 41syl 17 . . . . . 6 (𝜑𝐴 ∈ Grp)
43 eqid 2621 . . . . . . . 8 (1r𝐴) = (1r𝐴)
4435, 43ringidcl 18508 . . . . . . 7 (𝐴 ∈ Ring → (1r𝐴) ∈ 𝐵)
4540, 44syl 17 . . . . . 6 (𝜑 → (1r𝐴) ∈ 𝐵)
46 eqid 2621 . . . . . . 7 (invg𝐴) = (invg𝐴)
4735, 46grpinvcl 17407 . . . . . 6 ((𝐴 ∈ Grp ∧ (1r𝐴) ∈ 𝐵) → ((invg𝐴)‘(1r𝐴)) ∈ 𝐵)
4842, 45, 47syl2anc 692 . . . . 5 (𝜑 → ((invg𝐴)‘(1r𝐴)) ∈ 𝐵)
49 eqid 2621 . . . . . 6 (.r𝐴) = (.r𝐴)
5035, 49ringcl 18501 . . . . 5 ((𝐴 ∈ Ring ∧ 𝑣𝐵 ∧ ((invg𝐴)‘(1r𝐴)) ∈ 𝐵) → (𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) ∈ 𝐵)
5140, 33, 48, 50syl3anc 1323 . . . 4 (𝜑 → (𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) ∈ 𝐵)
5251, 36eleqtrrd 2701 . . 3 (𝜑 → (𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) ∈ (Base‘(Scalar‘𝐶)))
5345, 36eleqtrrd 2701 . . 3 (𝜑 → (1r𝐴) ∈ (Base‘(Scalar‘𝐶)))
54 mapdpglem28.ue . . . . 5 (𝜑𝑢𝐵)
5535, 49ringcl 18501 . . . . 5 ((𝐴 ∈ Ring ∧ 𝑢𝐵 ∧ ((invg𝐴)‘(1r𝐴)) ∈ 𝐵) → (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) ∈ 𝐵)
5640, 54, 48, 55syl3anc 1323 . . . 4 (𝜑 → (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) ∈ 𝐵)
5756, 36eleqtrrd 2701 . . 3 (𝜑 → (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) ∈ (Base‘(Scalar‘𝐶)))
58 mapdpglem26.o . . . 4 𝑂 = (0g𝐴)
59 mapdpglem28.u1 . . . 4 (𝜑 = (𝑢 · 𝑖))
60 mapdpglem28.u2 . . . 4 (𝜑 → (𝐺𝑅) = (𝑣 · (𝐺𝑅𝑖)))
618, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27, 34, 35, 5, 58, 33, 59, 60mapdpglem29 36508 . . 3 (𝜑 → (𝐽‘{𝐺}) ≠ (𝐽‘{𝑖}))
628, 14, 34, 35, 49, 9, 1, 5, 10, 48, 54, 28lcdvsass 36415 . . . . 5 (𝜑 → ((𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖) = (((invg𝐴)‘(1r𝐴)) · (𝑢 · 𝑖)))
6362oveq2d 6631 . . . 4 (𝜑 → (((1r𝐴) · 𝐺)(+g𝐶)((𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖)) = (((1r𝐴) · 𝐺)(+g𝐶)(((invg𝐴)‘(1r𝐴)) · (𝑢 · 𝑖))))
648, 14, 34, 35, 9, 1, 5, 10, 45, 12lcdvscl 36413 . . . . 5 (𝜑 → ((1r𝐴) · 𝐺) ∈ 𝐹)
658, 14, 34, 35, 9, 1, 5, 10, 54, 28lcdvscl 36413 . . . . 5 (𝜑 → (𝑢 · 𝑖) ∈ 𝐹)
668, 14, 34, 46, 43, 9, 1, 2, 5, 19, 10, 64, 65lcdvsub 36425 . . . 4 (𝜑 → (((1r𝐴) · 𝐺)𝑅(𝑢 · 𝑖)) = (((1r𝐴) · 𝐺)(+g𝐶)(((invg𝐴)‘(1r𝐴)) · (𝑢 · 𝑖))))
678, 14, 34, 35, 49, 9, 1, 5, 10, 48, 33, 28lcdvsass 36415 . . . . . 6 (𝜑 → ((𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖) = (((invg𝐴)‘(1r𝐴)) · (𝑣 · 𝑖)))
6867oveq2d 6631 . . . . 5 (𝜑 → ((𝑣 · 𝐺)(+g𝐶)((𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖)) = ((𝑣 · 𝐺)(+g𝐶)(((invg𝐴)‘(1r𝐴)) · (𝑣 · 𝑖))))
698, 14, 34, 35, 9, 1, 5, 10, 33, 12lcdvscl 36413 . . . . . 6 (𝜑 → (𝑣 · 𝐺) ∈ 𝐹)
708, 14, 34, 35, 9, 1, 5, 10, 33, 28lcdvscl 36413 . . . . . 6 (𝜑 → (𝑣 · 𝑖) ∈ 𝐹)
718, 14, 34, 46, 43, 9, 1, 2, 5, 19, 10, 69, 70lcdvsub 36425 . . . . 5 (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = ((𝑣 · 𝐺)(+g𝐶)(((invg𝐴)‘(1r𝐴)) · (𝑣 · 𝑖))))
728, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27, 34, 35, 5, 58, 33, 59, 60mapdpglem28 36509 . . . . . 6 (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = (𝐺𝑅(𝑢 · 𝑖)))
73 eqid 2621 . . . . . . . . . 10 (1r‘(Scalar‘𝐶)) = (1r‘(Scalar‘𝐶))
748, 14, 34, 43, 9, 3, 73, 10lcd1 36417 . . . . . . . . 9 (𝜑 → (1r‘(Scalar‘𝐶)) = (1r𝐴))
7574oveq1d 6630 . . . . . . . 8 (𝜑 → ((1r‘(Scalar‘𝐶)) · 𝐺) = ((1r𝐴) · 𝐺))
768, 9, 10lcdlmod 36400 . . . . . . . . 9 (𝜑𝐶 ∈ LMod)
771, 3, 5, 73lmodvs1 18831 . . . . . . . . 9 ((𝐶 ∈ LMod ∧ 𝐺𝐹) → ((1r‘(Scalar‘𝐶)) · 𝐺) = 𝐺)
7876, 12, 77syl2anc 692 . . . . . . . 8 (𝜑 → ((1r‘(Scalar‘𝐶)) · 𝐺) = 𝐺)
7975, 78eqtr3d 2657 . . . . . . 7 (𝜑 → ((1r𝐴) · 𝐺) = 𝐺)
8079oveq1d 6630 . . . . . 6 (𝜑 → (((1r𝐴) · 𝐺)𝑅(𝑢 · 𝑖)) = (𝐺𝑅(𝑢 · 𝑖)))
8172, 80eqtr4d 2658 . . . . 5 (𝜑 → ((𝑣 · 𝐺)𝑅(𝑣 · 𝑖)) = (((1r𝐴) · 𝐺)𝑅(𝑢 · 𝑖)))
8268, 71, 813eqtr2rd 2662 . . . 4 (𝜑 → (((1r𝐴) · 𝐺)𝑅(𝑢 · 𝑖)) = ((𝑣 · 𝐺)(+g𝐶)((𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖)))
8363, 66, 823eqtr2rd 2662 . . 3 (𝜑 → ((𝑣 · 𝐺)(+g𝐶)((𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖)) = (((1r𝐴) · 𝐺)(+g𝐶)((𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) · 𝑖)))
841, 2, 3, 4, 5, 6, 7, 11, 26, 32, 37, 52, 53, 57, 61, 83lvecindp2 19079 . 2 (𝜑 → (𝑣 = (1r𝐴) ∧ (𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) = (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴)))))
8535, 49, 43, 46, 40, 33rngnegr 18535 . . . . 5 (𝜑 → (𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) = ((invg𝐴)‘𝑣))
8635, 49, 43, 46, 40, 54rngnegr 18535 . . . . 5 (𝜑 → (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) = ((invg𝐴)‘𝑢))
8785, 86eqeq12d 2636 . . . 4 (𝜑 → ((𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) = (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) ↔ ((invg𝐴)‘𝑣) = ((invg𝐴)‘𝑢)))
8835, 46, 42, 33, 54grpinv11 17424 . . . 4 (𝜑 → (((invg𝐴)‘𝑣) = ((invg𝐴)‘𝑢) ↔ 𝑣 = 𝑢))
8987, 88bitrd 268 . . 3 (𝜑 → ((𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) = (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴))) ↔ 𝑣 = 𝑢))
9089anbi2d 739 . 2 (𝜑 → ((𝑣 = (1r𝐴) ∧ (𝑣(.r𝐴)((invg𝐴)‘(1r𝐴))) = (𝑢(.r𝐴)((invg𝐴)‘(1r𝐴)))) ↔ (𝑣 = (1r𝐴) ∧ 𝑣 = 𝑢)))
9184, 90mpbid 222 1 (𝜑 → (𝑣 = (1r𝐴) ∧ 𝑣 = 𝑢))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790   ∖ cdif 3557  {csn 4155  ‘cfv 5857  (class class class)co 6615  Basecbs 15800  +gcplusg 15881  .rcmulr 15882  Scalarcsca 15884   ·𝑠 cvsca 15885  0gc0g 16040  Grpcgrp 17362  invgcminusg 17363  -gcsg 17364  1rcur 18441  Ringcrg 18487  LModclmod 18803  LSpanclspn 18911  HLchlt 34156  LHypclh 34789  DVecHcdvh 35886  LCDualclcd 36394  mapdcmpd 36432 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-riotaBAD 33758 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-tpos 7312  df-undef 7359  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-map 7819  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-n0 11253  df-z 11338  df-uz 11648  df-fz 12285  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-sca 15897  df-vsca 15898  df-0g 16042  df-mre 16186  df-mrc 16187  df-acs 16189  df-preset 16868  df-poset 16886  df-plt 16898  df-lub 16914  df-glb 16915  df-join 16916  df-meet 16917  df-p0 16979  df-p1 16980  df-lat 16986  df-clat 17048  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-grp 17365  df-minusg 17366  df-sbg 17367  df-subg 17531  df-cntz 17690  df-oppg 17716  df-lsm 17991  df-cmn 18135  df-abl 18136  df-mgp 18430  df-ur 18442  df-ring 18489  df-oppr 18563  df-dvdsr 18581  df-unit 18582  df-invr 18612  df-dvr 18623  df-drng 18689  df-lmod 18805  df-lss 18873  df-lsp 18912  df-lvec 19043  df-lsatoms 33782  df-lshyp 33783  df-lcv 33825  df-lfl 33864  df-lkr 33892  df-ldual 33930  df-oposet 33982  df-ol 33984  df-oml 33985  df-covers 34072  df-ats 34073  df-atl 34104  df-cvlat 34128  df-hlat 34157  df-llines 34303  df-lplanes 34304  df-lvols 34305  df-lines 34306  df-psubsp 34308  df-pmap 34309  df-padd 34601  df-lhyp 34793  df-laut 34794  df-ldil 34909  df-ltrn 34910  df-trl 34965  df-tgrp 35550  df-tendo 35562  df-edring 35564  df-dveca 35810  df-disoa 35837  df-dvech 35887  df-dib 35947  df-dic 35981  df-dih 36037  df-doch 36156  df-djh 36203  df-lcdual 36395  df-mapd 36433 This theorem is referenced by:  mapdpglem31  36511
 Copyright terms: Public domain W3C validator