Theorem diaocN 38294

Description: Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom 𝑊). (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
diaoc.j	⊢ ∨ = (join‘𝐾)
diaoc.m	⊢ ∧ = (meet‘𝐾)
diaoc.o	⊢ ⊥ = (oc‘𝐾)
diaoc.h	⊢ 𝐻 = (LHyp‘𝐾)
diaoc.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
diaoc.i	⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
diaoc.n	⊢ 𝑁 = ((ocA‘𝐾)‘𝑊)

Assertion

Ref	Expression
diaocN	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝑁‘(𝐼‘𝑋)))

Proof of Theorem diaocN

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 485	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		eqid 2820	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		diaoc.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
4		diaoc.i	. . . . 5 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
5	2, 3, 4	diadmclN 38206	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
6		eqid 2820	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
7	6, 3, 4	diadmleN 38207	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
8		diaoc.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9	2, 6, 3, 8, 4	diass 38211	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑋(le‘𝐾)𝑊)) → (𝐼‘𝑋) ⊆ 𝑇)
10	1, 5, 7, 9	syl12anc 834	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ⊆ 𝑇)
11		diaoc.j	. . . 4 ⊢ ∨ = (join‘𝐾)
12		diaoc.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
13		diaoc.o	. . . 4 ⊢ ⊥ = (oc‘𝐾)
14		diaoc.n	. . . 4 ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊)
15	11, 12, 13, 3, 8, 4, 14	docavalN 38292	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ⊆ 𝑇) → (𝑁‘(𝐼‘𝑋)) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))
16	10, 15	syldan 593	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝑁‘(𝐼‘𝑋)) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))
17	3, 4	diaclN 38219	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼)
18		intmin 4889	. . . . . . . 8 ⊢ ((𝐼‘𝑋) ∈ ran 𝐼 → ∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧} = (𝐼‘𝑋))
19	17, 18	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → ∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧} = (𝐼‘𝑋))
20	19	fveq2d 6667	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧}) = (◡𝐼‘(𝐼‘𝑋)))
21	3, 4	diaf11N 38218	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼)
22		f1ocnvfv1 7026	. . . . . . 7 ⊢ ((𝐼:dom 𝐼–1-1-onto→ran 𝐼 ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘(𝐼‘𝑋)) = 𝑋)
23	21, 22	sylan 582	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘(𝐼‘𝑋)) = 𝑋)
24	20, 23	eqtrd 2855	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧}) = 𝑋)
25	24	fveq2d 6667	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → ( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) = ( ⊥ ‘𝑋))
26	25	oveq1d 7164	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)))
27	26	fvoveq1d 7171	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))
28	16, 27	eqtr2d 2856	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝑁‘(𝐼‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  {crab 3141   ⊆ wss 3929  ∩ cint 4869   class class class wbr 5059  ^◡ccnv 5547  dom cdm 5548  ran crn 5549  –1-1-onto→wf1o 6347  ‘cfv 6348  (class class class)co 7149  Basecbs 16478  lecple 16567  occoc 16568  joincjn 17549  meetcmee 17550  HLchlt 36519  LHypclh 37153  LTrncltrn 37270  DIsoAcdia 38197  ocAcocaN 38288

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 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454  ax-riotaBAD 36122

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-int 4870  df-iun 4914  df-iin 4915  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1st 7682  df-2nd 7683  df-undef 7932  df-map 8401  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36345  df-ol 36347  df-oml 36348  df-covers 36435  df-ats 36436  df-atl 36467  df-cvlat 36491  df-hlat 36520  df-llines 36667  df-lplanes 36668  df-lvols 36669  df-lines 36670  df-psubsp 36672  df-pmap 36673  df-padd 36965  df-lhyp 37157  df-laut 37158  df-ldil 37273  df-ltrn 37274  df-trl 37328  df-disoa 38198  df-docaN 38289

This theorem is referenced by:  doca2N  38295  djajN  38306