dihjatcclem2 - Mathbox for Norm Megill

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

Theorem dihjatcclem2 37948

Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014.)

**Hypotheses**
Ref	Expression
dihjatcclem.b	⊢ 𝐵 = (Base‘𝐾)
dihjatcclem.l	⊢ ≤ = (le‘𝐾)
dihjatcclem.h	⊢ 𝐻 = (LHyp‘𝐾)
dihjatcclem.j	⊢ ∨ = (join‘𝐾)
dihjatcclem.m	⊢ ∧ = (meet‘𝐾)
dihjatcclem.a	⊢ 𝐴 = (Atoms‘𝐾)
dihjatcclem.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihjatcclem.s	⊢ ⊕ = (LSSum‘𝑈)
dihjatcclem.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihjatcclem.v	⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
dihjatcclem.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dihjatcclem.p	⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
dihjatcclem.q	⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
dihjatcclem2.c	⊢ (𝜑 → (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))

**Assertion**
Ref	Expression
dihjatcclem2	⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))

**Proof of Theorem dihjatcclem2**
Step	Hyp	Ref	Expression
1		dihjatcclem.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		dihjatcclem.l	. . 3 ⊢ ≤ = (le‘𝐾)
3		dihjatcclem.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
4		dihjatcclem.j	. . 3 ⊢ ∨ = (join‘𝐾)
5		dihjatcclem.m	. . 3 ⊢ ∧ = (meet‘𝐾)
6		dihjatcclem.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
7		dihjatcclem.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
8		dihjatcclem.s	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
9		dihjatcclem.i	. . 3 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
10		dihjatcclem.v	. . 3 ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
11		dihjatcclem.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		dihjatcclem.p	. . 3 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
13		dihjatcclem.q	. . 3 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
14	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	dihjatcclem1 37947	. 2 ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉)))
15	3, 7, 11	dvhlmod 37639	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
16		eqid 2772	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
17	16	lsssssubg 19442	. . . . 5 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
18	15, 17	syl 17	. . . 4 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
19	12	simpld 487	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
20	1, 6	atbase 35818	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
21	19, 20	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
22	1, 3, 9, 7, 16	dihlss 37779	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐵) → (𝐼‘𝑃) ∈ (LSubSp‘𝑈))
23	11, 21, 22	syl2anc 576	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑃) ∈ (LSubSp‘𝑈))
24	13	simpld 487	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
25	1, 6	atbase 35818	. . . . . . 7 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
26	24, 25	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ 𝐵)
27	1, 3, 9, 7, 16	dihlss 37779	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐵) → (𝐼‘𝑄) ∈ (LSubSp‘𝑈))
28	11, 26, 27	syl2anc 576	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑄) ∈ (LSubSp‘𝑈))
29	16, 8	lsmcl 19567	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ (𝐼‘𝑃) ∈ (LSubSp‘𝑈) ∧ (𝐼‘𝑄) ∈ (LSubSp‘𝑈)) → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ∈ (LSubSp‘𝑈))
30	15, 23, 28, 29	syl3anc 1351	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ∈ (LSubSp‘𝑈))
31	18, 30	sseldd 3855	. . 3 ⊢ (𝜑 → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ∈ (SubGrp‘𝑈))
32	10	fveq2i 6496	. . . . 5 ⊢ (𝐼‘𝑉) = (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊))
33	11	simpld 487	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ HL)
34	33	hllatd 35893	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Lat)
35	1, 4, 6	hlatjcl 35896	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
36	33, 19, 24, 35	syl3anc 1351	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ 𝐵)
37	11	simprd 488	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ 𝐻)
38	1, 3	lhpbase 36527	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
39	37, 38	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ 𝐵)
40	1, 5	latmcl 17510	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐵)
41	34, 36, 39, 40	syl3anc 1351	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐵)
42	1, 3, 9, 7, 16	dihlss 37779	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐵) → (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)) ∈ (LSubSp‘𝑈))
43	11, 41, 42	syl2anc 576	. . . . 5 ⊢ (𝜑 → (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)) ∈ (LSubSp‘𝑈))
44	32, 43	syl5eqel 2864	. . . 4 ⊢ (𝜑 → (𝐼‘𝑉) ∈ (LSubSp‘𝑈))
45	18, 44	sseldd 3855	. . 3 ⊢ (𝜑 → (𝐼‘𝑉) ∈ (SubGrp‘𝑈))
46		dihjatcclem2.c	. . 3 ⊢ (𝜑 → (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
47	8	lsmss2 18542	. . 3 ⊢ ((((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑉) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) → (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
48	31, 45, 46, 47	syl3anc 1351	. 2 ⊢ (𝜑 → (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
49	14, 48	eqtrd 2808	1 ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2048 ⊆ wss 3825 class class class wbr 4923 ‘cfv 6182 (class class class)co 6970 Basecbs 16329 lecple 16418 joincjn 17402 meetcmee 17403 Latclat 17503 SubGrpcsubg 18047 LSSumclsm 18510 LModclmod 19346 LSubSpclss 19415 Atomscatm 35792 HLchlt 35879 LHypclh 36513 DVecHcdvh 37607 DIsoHcdih 37757

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 ax-riotaBAD 35482

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-iin 4789 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7494 df-2nd 7495 df-tpos 7688 df-undef 7735 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-1o 7897 df-oadd 7901 df-er 8081 df-map 8200 df-en 8299 df-dom 8300 df-sdom 8301 df-fin 8302 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-nn 11432 df-2 11496 df-3 11497 df-4 11498 df-5 11499 df-6 11500 df-n0 11701 df-z 11787 df-uz 12052 df-fz 12702 df-struct 16331 df-ndx 16332 df-slot 16333 df-base 16335 df-sets 16336 df-ress 16337 df-plusg 16424 df-mulr 16425 df-sca 16427 df-vsca 16428 df-0g 16561 df-proset 17386 df-poset 17404 df-plt 17416 df-lub 17432 df-glb 17433 df-join 17434 df-meet 17435 df-p0 17497 df-p1 17498 df-lat 17504 df-clat 17566 df-mgm 17700 df-sgrp 17742 df-mnd 17753 df-submnd 17794 df-grp 17884 df-minusg 17885 df-sbg 17886 df-subg 18050 df-cntz 18208 df-lsm 18512 df-cmn 18658 df-abl 18659 df-mgp 18953 df-ur 18965 df-ring 19012 df-oppr 19086 df-dvdsr 19104 df-unit 19105 df-invr 19135 df-dvr 19146 df-drng 19217 df-lmod 19348 df-lss 19416 df-lsp 19456 df-lvec 19587 df-oposet 35705 df-ol 35707 df-oml 35708 df-covers 35795 df-ats 35796 df-atl 35827 df-cvlat 35851 df-hlat 35880 df-llines 36027 df-lplanes 36028 df-lvols 36029 df-lines 36030 df-psubsp 36032 df-pmap 36033 df-padd 36325 df-lhyp 36517 df-laut 36518 df-ldil 36633 df-ltrn 36634 df-trl 36688 df-tendo 37284 df-edring 37286 df-disoa 37558 df-dvech 37608 df-dib 37668 df-dic 37702 df-dih 37758

This theorem is referenced by: dihjatcc 37951

W3C validator