Theorem dihjatb 39336

Description: Isomorphism H of lattice join of two atoms under the fiducial hyperplane. (Contributed by NM, 23-Sep-2014.)

Hypotheses

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

Assertion

Ref	Expression
dihjatb	⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))

Proof of Theorem dihjatb

Step	Hyp	Ref	Expression
1		dihjatb.l	. . 3 ⊢ ≤ = (le‘𝐾)
2		dihjatb.j	. . 3 ⊢ ∨ = (join‘𝐾)
3		dihjatb.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4		dihjatb.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
5		dihjatb.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6		dihjatb.s	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
7		dihjatb.i	. . 3 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
8		dihjatb.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9		dihjatb.p	. . 3 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊))
10		dihjatb.q	. . 3 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊))
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	dih2dimb 39164	. 2 ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) ⊆ ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))
12		eqid 2739	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
13	9	simpld 498	. . . 4 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
14	12, 3	atbase 37209	. . . 4 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
15	13, 14	syl 17	. . 3 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾))
16	10	simpld 498	. . . 4 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
17	12, 3	atbase 37209	. . . 4 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
18	16, 17	syl 17	. . 3 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾))
19	12, 4, 2, 5, 6, 7, 8, 15, 18	dihsumssj 39328	. 2 ⊢ (𝜑 → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊆ (𝐼‘(𝑃 ∨ 𝑄)))
20	11, 19	eqssd 3935	1 ⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112   class class class wbr 5070  ‘cfv 6415  (class class class)co 7252  Basecbs 16815  lecple 16870  joincjn 17919  LSSumclsm 19129  Atomscatm 37183  HLchlt 37270  LHypclh 37904  DVecHcdvh 38998  DIsoHcdih 39148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5203  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563  ax-cnex 10833  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-addrcl 10838  ax-mulcl 10839  ax-mulrcl 10840  ax-mulcom 10841  ax-addass 10842  ax-mulass 10843  ax-distr 10844  ax-i2m1 10845  ax-1ne0 10846  ax-1rid 10847  ax-rnegex 10848  ax-rrecex 10849  ax-cnre 10850  ax-pre-lttri 10851  ax-pre-lttrn 10852  ax-pre-ltadd 10853  ax-pre-mulgt0 10854  ax-riotaBAD 36873

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-riota 7209  df-ov 7255  df-oprab 7256  df-mpo 7257  df-om 7685  df-1st 7801  df-2nd 7802  df-tpos 8010  df-undef 8057  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-1o 8244  df-er 8433  df-map 8552  df-en 8669  df-dom 8670  df-sdom 8671  df-fin 8672  df-pnf 10917  df-mnf 10918  df-xr 10919  df-ltxr 10920  df-le 10921  df-sub 11112  df-neg 11113  df-nn 11879  df-2 11941  df-3 11942  df-4 11943  df-5 11944  df-6 11945  df-n0 12139  df-z 12225  df-uz 12487  df-fz 13144  df-struct 16751  df-sets 16768  df-slot 16786  df-ndx 16798  df-base 16816  df-ress 16843  df-plusg 16876  df-mulr 16877  df-sca 16879  df-vsca 16880  df-0g 17044  df-proset 17903  df-poset 17921  df-plt 17938  df-lub 17954  df-glb 17955  df-join 17956  df-meet 17957  df-p0 18033  df-p1 18034  df-lat 18040  df-clat 18107  df-mgm 18216  df-sgrp 18265  df-mnd 18276  df-submnd 18321  df-grp 18470  df-minusg 18471  df-sbg 18472  df-subg 18642  df-cntz 18813  df-lsm 19131  df-cmn 19278  df-abl 19279  df-mgp 19611  df-ur 19628  df-ring 19675  df-oppr 19752  df-dvdsr 19773  df-unit 19774  df-invr 19804  df-dvr 19815  df-drng 19883  df-lmod 20015  df-lss 20084  df-lsp 20124  df-lvec 20255  df-lsatoms 36896  df-oposet 37096  df-ol 37098  df-oml 37099  df-covers 37186  df-ats 37187  df-atl 37218  df-cvlat 37242  df-hlat 37271  df-llines 37418  df-lplanes 37419  df-lvols 37420  df-lines 37421  df-psubsp 37423  df-pmap 37424  df-padd 37716  df-lhyp 37908  df-laut 37909  df-ldil 38024  df-ltrn 38025  df-trl 38079  df-tgrp 38663  df-tendo 38675  df-edring 38677  df-dveca 38923  df-disoa 38949  df-dvech 38999  df-dib 39059  df-dic 39093  df-dih 39149  df-doch 39268  df-djh 39315

This theorem is referenced by:  dihjat  39343