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

Theorem mapdordlem1a 39687
Description: Lemma for mapdord 39691. (Contributed by NM, 27-Jan-2015.)
Hypotheses
Ref Expression
mapdordlem1a.h 𝐻 = (LHypβ€˜πΎ)
mapdordlem1a.o 𝑂 = ((ocHβ€˜πΎ)β€˜π‘Š)
mapdordlem1a.u π‘ˆ = ((DVecHβ€˜πΎ)β€˜π‘Š)
mapdordlem1a.v 𝑉 = (Baseβ€˜π‘ˆ)
mapdordlem1a.y π‘Œ = (LSHypβ€˜π‘ˆ)
mapdordlem1a.f 𝐹 = (LFnlβ€˜π‘ˆ)
mapdordlem1a.l 𝐿 = (LKerβ€˜π‘ˆ)
mapdordlem1a.t 𝑇 = {𝑔 ∈ 𝐹 ∣ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π‘”))) ∈ π‘Œ}
mapdordlem1a.c 𝐢 = {𝑔 ∈ 𝐹 ∣ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π‘”))) = (πΏβ€˜π‘”)}
mapdordlem1a.k (πœ‘ β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
Assertion
Ref Expression
mapdordlem1a (πœ‘ β†’ (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐢 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)))
Distinct variable groups:   𝑔,𝐹   𝑔,𝐽   𝑔,𝐿   𝑔,𝑂   𝑔,π‘Œ
Allowed substitution hints:   πœ‘(𝑔)   𝐢(𝑔)   𝑇(𝑔)   π‘ˆ(𝑔)   𝐻(𝑔)   𝐾(𝑔)   𝑉(𝑔)   π‘Š(𝑔)

Proof of Theorem mapdordlem1a
StepHypRef Expression
1 simprr 771 . . . . . 6 ((πœ‘ ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) β†’ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)
2 mapdordlem1a.h . . . . . . 7 𝐻 = (LHypβ€˜πΎ)
3 mapdordlem1a.o . . . . . . 7 𝑂 = ((ocHβ€˜πΎ)β€˜π‘Š)
4 mapdordlem1a.u . . . . . . 7 π‘ˆ = ((DVecHβ€˜πΎ)β€˜π‘Š)
5 mapdordlem1a.f . . . . . . 7 𝐹 = (LFnlβ€˜π‘ˆ)
6 mapdordlem1a.y . . . . . . 7 π‘Œ = (LSHypβ€˜π‘ˆ)
7 mapdordlem1a.l . . . . . . 7 𝐿 = (LKerβ€˜π‘ˆ)
8 mapdordlem1a.k . . . . . . . 8 (πœ‘ β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
98adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
10 simprl 769 . . . . . . 7 ((πœ‘ ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) β†’ 𝐽 ∈ 𝐹)
112, 3, 4, 5, 6, 7, 9, 10dochlkr 39438 . . . . . 6 ((πœ‘ ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) β†’ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ ↔ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (πΏβ€˜π½) ∈ π‘Œ)))
121, 11mpbid 232 . . . . 5 ((πœ‘ ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) β†’ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (πΏβ€˜π½) ∈ π‘Œ))
1312simpld 496 . . . 4 ((πœ‘ ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) β†’ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½))
1413ex 414 . . 3 (πœ‘ β†’ ((𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ) β†’ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½)))
1514pm4.71rd 564 . 2 (πœ‘ β†’ ((𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ) ↔ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ))))
16 2fveq3 6805 . . . . 5 (𝑔 = 𝐽 β†’ (π‘‚β€˜(πΏβ€˜π‘”)) = (π‘‚β€˜(πΏβ€˜π½)))
1716fveq2d 6804 . . . 4 (𝑔 = 𝐽 β†’ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π‘”))) = (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))))
1817eleq1d 2821 . . 3 (𝑔 = 𝐽 β†’ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π‘”))) ∈ π‘Œ ↔ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ))
19 mapdordlem1a.t . . 3 𝑇 = {𝑔 ∈ 𝐹 ∣ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π‘”))) ∈ π‘Œ}
2018, 19elrab2 3632 . 2 (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ))
21 mapdordlem1a.c . . . . 5 𝐢 = {𝑔 ∈ 𝐹 ∣ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π‘”))) = (πΏβ€˜π‘”)}
2221lcfl1lem 39544 . . . 4 (𝐽 ∈ 𝐢 ↔ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½)))
2322anbi1i 625 . . 3 ((𝐽 ∈ 𝐢 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ) ↔ ((𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½)) ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ))
24 anass 470 . . 3 (((𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½)) ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ) ↔ (𝐽 ∈ 𝐹 ∧ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)))
25 an12 643 . . 3 ((𝐽 ∈ 𝐹 ∧ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)) ↔ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)))
2623, 24, 253bitri 298 . 2 ((𝐽 ∈ 𝐢 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ) ↔ ((π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) = (πΏβ€˜π½) ∧ (𝐽 ∈ 𝐹 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)))
2715, 20, 263bitr4g 315 1 (πœ‘ β†’ (𝐽 ∈ 𝑇 ↔ (𝐽 ∈ 𝐢 ∧ (π‘‚β€˜(π‘‚β€˜(πΏβ€˜π½))) ∈ π‘Œ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104  {crab 3284  β€˜cfv 6454  Basecbs 16953  LSHypclsh 37028  LFnlclfn 37110  LKerclk 37138  HLchlt 37403  LHypclh 38037  DVecHcdvh 39131  ocHcoch 39400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-cnex 10969  ax-resscn 10970  ax-1cn 10971  ax-icn 10972  ax-addcl 10973  ax-addrcl 10974  ax-mulcl 10975  ax-mulrcl 10976  ax-mulcom 10977  ax-addass 10978  ax-mulass 10979  ax-distr 10980  ax-i2m1 10981  ax-1ne0 10982  ax-1rid 10983  ax-rnegex 10984  ax-rrecex 10985  ax-cnre 10986  ax-pre-lttri 10987  ax-pre-lttrn 10988  ax-pre-ltadd 10989  ax-pre-mulgt0 10990  ax-riotaBAD 37006
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-tp 4570  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-iin 4934  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-riota 7260  df-ov 7306  df-oprab 7307  df-mpo 7308  df-om 7741  df-1st 7859  df-2nd 7860  df-tpos 8069  df-undef 8116  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-1o 8324  df-er 8525  df-map 8644  df-en 8761  df-dom 8762  df-sdom 8763  df-fin 8764  df-pnf 11053  df-mnf 11054  df-xr 11055  df-ltxr 11056  df-le 11057  df-sub 11249  df-neg 11250  df-nn 12016  df-2 12078  df-3 12079  df-4 12080  df-5 12081  df-6 12082  df-n0 12276  df-z 12362  df-uz 12625  df-fz 13282  df-struct 16889  df-sets 16906  df-slot 16924  df-ndx 16936  df-base 16954  df-ress 16983  df-plusg 17016  df-mulr 17017  df-sca 17019  df-vsca 17020  df-0g 17193  df-proset 18054  df-poset 18072  df-plt 18089  df-lub 18105  df-glb 18106  df-join 18107  df-meet 18108  df-p0 18184  df-p1 18185  df-lat 18191  df-clat 18258  df-mgm 18367  df-sgrp 18416  df-mnd 18427  df-submnd 18472  df-grp 18621  df-minusg 18622  df-sbg 18623  df-subg 18793  df-cntz 18964  df-lsm 19282  df-cmn 19429  df-abl 19430  df-mgp 19762  df-ur 19779  df-ring 19826  df-oppr 19903  df-dvdsr 19924  df-unit 19925  df-invr 19955  df-dvr 19966  df-drng 20034  df-lmod 20166  df-lss 20235  df-lsp 20275  df-lvec 20406  df-lsatoms 37029  df-lshyp 37030  df-lfl 37111  df-lkr 37139  df-oposet 37229  df-ol 37231  df-oml 37232  df-covers 37319  df-ats 37320  df-atl 37351  df-cvlat 37375  df-hlat 37404  df-llines 37551  df-lplanes 37552  df-lvols 37553  df-lines 37554  df-psubsp 37556  df-pmap 37557  df-padd 37849  df-lhyp 38041  df-laut 38042  df-ldil 38157  df-ltrn 38158  df-trl 38212  df-tendo 38808  df-edring 38810  df-disoa 39082  df-dvech 39132  df-dib 39192  df-dic 39226  df-dih 39282  df-doch 39401
This theorem is referenced by:  mapdordlem2  39690
  Copyright terms: Public domain W3C validator