![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihsumssj | Unicode version |
Description: The subspace sum of two isomorphisms of lattice elements is less than the isomorphism of their lattice join. (Contributed by NM, 23-Sep-2014.) |
Ref | Expression |
---|---|
dihsumssj.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.j |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.u |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
dihsumssj.y |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
dihsumssj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihsumssj.h |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dihsumssj.u |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqid 2404 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dihsumssj.p |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2404 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | dihsumssj.k |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | dihsumssj.x |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | dihsumssj.b |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | dihsumssj.i |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 8, 1, 9, 2, 3 | dihss 31734 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 6, 7, 10 | syl2anc 643 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | dihsumssj.y |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 8, 1, 9, 2, 3 | dihss 31734 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 6, 12, 13 | syl2anc 643 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 2, 3, 4, 5, 6, 11, 14 | djhsumss 31890 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | dihsumssj.j |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
17 | 8, 16, 1, 9, 5 | djhlj 31884 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 6, 7, 12, 17 | syl12anc 1182 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 15, 18 | sseqtr4d 3345 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: dihjatb 31899 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-fal 1326 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-tpos 6438 df-undef 6502 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-sca 13500 df-vsca 13501 df-0g 13682 df-poset 14358 df-plt 14370 df-lub 14386 df-glb 14387 df-join 14388 df-meet 14389 df-p0 14423 df-p1 14424 df-lat 14430 df-clat 14492 df-mnd 14645 df-submnd 14694 df-grp 14767 df-minusg 14768 df-sbg 14769 df-subg 14896 df-cntz 15071 df-lsm 15225 df-cmn 15369 df-abl 15370 df-mgp 15604 df-rng 15618 df-ur 15620 df-oppr 15683 df-dvdsr 15701 df-unit 15702 df-invr 15732 df-dvr 15743 df-drng 15792 df-lmod 15907 df-lss 15964 df-lsp 16003 df-lvec 16130 df-lsatoms 29459 df-oposet 29659 df-ol 29661 df-oml 29662 df-covers 29749 df-ats 29750 df-atl 29781 df-cvlat 29805 df-hlat 29834 df-llines 29980 df-lplanes 29981 df-lvols 29982 df-lines 29983 df-psubsp 29985 df-pmap 29986 df-padd 30278 df-lhyp 30470 df-laut 30471 df-ldil 30586 df-ltrn 30587 df-trl 30641 df-tendo 31237 df-edring 31239 df-disoa 31512 df-dvech 31562 df-dib 31622 df-dic 31656 df-dih 31712 df-doch 31831 df-djh 31878 |
Copyright terms: Public domain | W3C validator |