dihjat - Mathbox for Norm Megill

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

Theorem dihjat 42297

Description: Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014.)

**Hypotheses**
Ref	Expression
dihjat.h	⊢ 𝐻 = (LHyp‘𝐾)
dihjat.j	⊢ ∨ = (join‘𝐾)
dihjat.a	⊢ 𝐴 = (Atoms‘𝐾)
dihjat.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihjat.s	⊢ ⊕ = (LSSum‘𝑈)
dihjat.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihjat.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dihjat.p	⊢ (𝜑 → 𝑃 ∈ 𝐴)
dihjat.q	⊢ (𝜑 → 𝑄 ∈ 𝐴)

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

**Proof of Theorem dihjat**
Step	Hyp	Ref	Expression
1		eqid 2760	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
2		dihjat.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
3		dihjat.j	. . 3 ⊢ ∨ = (join‘𝐾)
4		dihjat.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
5		dihjat.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6		dihjat.s	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
7		dihjat.i	. . 3 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
8		dihjat.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10		dihjat.p	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
11	10	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ 𝐴)
12		simprl 783	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑃(le‘𝐾)𝑊)
13	11, 12	jca 521	. . 3 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ 𝐴 ∧ 𝑃(le‘𝐾)𝑊))
14		dihjat.q	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
15	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ 𝐴)
16		simprr 785	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄(le‘𝐾)𝑊)
17	15, 16	jca 521	. . 3 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ 𝐴 ∧ 𝑄(le‘𝐾)𝑊))
18	1, 2, 3, 4, 5, 6, 7, 9, 13, 17	dihjatb 42290	. 2 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
19		eqid 2760	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
21	19, 4	atbase 40163	. . . . . 6 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
22	10, 21	syl 18	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾))
23	22	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ (Base‘𝐾))
24		simprl 783	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑃(le‘𝐾)𝑊)
25	23, 24	jca 521	. . 3 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ (Base‘𝐾) ∧ 𝑃(le‘𝐾)𝑊))
26	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ 𝐴)
27		simprr 785	. . . 4 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑄(le‘𝐾)𝑊)
28	26, 27	jca 521	. . 3 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊))
29	19, 1, 2, 3, 4, 5, 6, 7, 20, 25, 28	dihjatc 42291	. 2 ⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
30	8	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
31	19, 4	atbase 40163	. . . . . . 7 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
32	14, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾))
33	32	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ (Base‘𝐾))
34		simprr 785	. . . . 5 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄(le‘𝐾)𝑊)
35	33, 34	jca 521	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ (Base‘𝐾) ∧ 𝑄(le‘𝐾)𝑊))
36	10	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ 𝐴)
37		simprl 783	. . . . 5 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑃(le‘𝐾)𝑊)
38	36, 37	jca 521	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊))
39	19, 1, 2, 3, 4, 5, 6, 7, 30, 35, 38	dihjatc 42291	. . 3 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑄 ∨ 𝑃)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃)))
40	8	simpld 500	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL)
41	3, 4	hlatjcom 40242	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
42	40, 10, 14, 41	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
43	42	fveq2d 6883	. . . 4 ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = (𝐼‘(𝑄 ∨ 𝑃)))
44	43	adantr 486	. . 3 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = (𝐼‘(𝑄 ∨ 𝑃)))
45	2, 5, 8	dvhlmod 41984	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LMod)
46		lmodabl 21094	. . . . . 6 ⊢ (𝑈 ∈ LMod → 𝑈 ∈ Abel)
47	45, 46	syl 18	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ Abel)
48		eqid 2760	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
49	48	lsssssubg 21143	. . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
50	45, 49	syl 18	. . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
51	19, 2, 7, 5, 48	dihlss 42124	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐼‘𝑃) ∈ (LSubSp‘𝑈))
52	8, 22, 51	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑃) ∈ (LSubSp‘𝑈))
53	50, 52	sseldd 3932	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑃) ∈ (SubGrp‘𝑈))
54	19, 2, 7, 5, 48	dihlss 42124	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝐼‘𝑄) ∈ (LSubSp‘𝑈))
55	8, 32, 54	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑄) ∈ (LSubSp‘𝑈))
56	50, 55	sseldd 3932	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑄) ∈ (SubGrp‘𝑈))
57	6	lsmcom 19986	. . . . 5 ⊢ ((𝑈 ∈ Abel ∧ (𝐼‘𝑃) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑄) ∈ (SubGrp‘𝑈)) → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃)))
58	47, 53, 56, 57	syl3anc 1398	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃)))
59	58	adantr 486	. . 3 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃)))
60	39, 44, 59	3eqtr4d 2805	. 2 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
61	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
62	10	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ 𝐴)
63		simprl 783	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑃(le‘𝐾)𝑊)
64	62, 63	jca 521	. . 3 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊))
65	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ 𝐴)
66		simprr 785	. . . 4 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑄(le‘𝐾)𝑊)
67	65, 66	jca 521	. . 3 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊))
68	1, 2, 3, 4, 5, 6, 7, 61, 64, 67	dihjatcc 42296	. 2 ⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
69	18, 29, 60, 68	4casesdan 1057	1 ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ⊆ wss 3899 class class class wbr 5103 ‘cfv 6533 (class class class)co 7414 Basecbs 17302 lecple 17350 joincjn 18400 SubGrpcsubg 19244 LSSumclsm 19762 Abelcabl 19909 LModclmod 21045 LSubSpclss 21116 Atomscatm 40137 HLchlt 40224 LHypclh 40858 DVecHcdvh 41952 DIsoHcdih 42102

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-riotaBAD 39827

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-tpos 8225 df-undef 8272 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-er 8697 df-map 8829 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-n0 12530 df-z 12617 df-uz 12889 df-fz 13563 df-struct 17240 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-mulr 17357 df-sca 17359 df-vsca 17360 df-0g 17527 df-proset 18383 df-poset 18402 df-plt 18417 df-lub 18433 df-glb 18434 df-join 18435 df-meet 18436 df-p0 18512 df-p1 18513 df-lat 18521 df-clat 18588 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-submnd 18893 df-grp 19061 df-minusg 19062 df-sbg 19063 df-subg 19247 df-cntz 19445 df-lsm 19764 df-cmn 19910 df-abl 19911 df-mgp 20275 df-rng 20289 df-ur 20322 df-ring 20375 df-oppr 20479 df-dvdsr 20499 df-unit 20500 df-invr 20530 df-dvr 20543 df-drng 20893 df-lmod 21047 df-lss 21117 df-lsp 21157 df-lvec 21288 df-lsatoms 39850 df-oposet 40050 df-ol 40052 df-oml 40053 df-covers 40140 df-ats 40141 df-atl 40172 df-cvlat 40196 df-hlat 40225 df-llines 40372 df-lplanes 40373 df-lvols 40374 df-lines 40375 df-psubsp 40377 df-pmap 40378 df-padd 40670 df-lhyp 40862 df-laut 40863 df-ldil 40978 df-ltrn 40979 df-trl 41033 df-tgrp 41617 df-tendo 41629 df-edring 41631 df-dveca 41877 df-disoa 41903 df-dvech 41953 df-dib 42013 df-dic 42047 df-dih 42103 df-doch 42222 df-djh 42269

This theorem is used by: dihprrnlem2 42299

W3C validator