Theorem diaocN 41464

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 482	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		eqid 2737	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		diaoc.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
4		diaoc.i	. . . . 5 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
5	2, 3, 4	diadmclN 41376	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
6		eqid 2737	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
7	6, 3, 4	diadmleN 41377	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
8		diaoc.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9	2, 6, 3, 8, 4	diass 41381	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑋(le‘𝐾)𝑊)) → (𝐼‘𝑋) ⊆ 𝑇)
10	1, 5, 7, 9	syl12anc 837	. . 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 41462	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ⊆ 𝑇) → (𝑁‘(𝐼‘𝑋)) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))
16	10, 15	syldan 592	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝑁‘(𝐼‘𝑋)) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))
17	3, 4	diaclN 41389	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼)
18		intmin 4924	. . . . . . . 8 ⊢ ((𝐼‘𝑋) ∈ ran 𝐼 → ∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧} = (𝐼‘𝑋))
19	17, 18	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → ∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧} = (𝐼‘𝑋))
20	19	fveq2d 6839	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧}) = (◡𝐼‘(𝐼‘𝑋)))
21	3, 4	diaf11N 41388	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼)
22		f1ocnvfv1 7225	. . . . . . 7 ⊢ ((𝐼:dom 𝐼–1-1-onto→ran 𝐼 ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘(𝐼‘𝑋)) = 𝑋)
23	21, 22	sylan 581	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘(𝐼‘𝑋)) = 𝑋)
24	20, 23	eqtrd 2772	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧}) = 𝑋)
25	24	fveq2d 6839	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → ( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) = ( ⊥ ‘𝑋))
26	25	oveq1d 7376	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)))
27	26	fvoveq1d 7383	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ (𝐼‘𝑋) ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))
28	16, 27	eqtr2d 2773	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝑁‘(𝐼‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3400   ⊆ wss 3902  ∩ cint 4903   class class class wbr 5099  ^◡ccnv 5624  dom cdm 5625  ran crn 5626  –1-1-onto→wf1o 6492  ‘cfv 6493  (class class class)co 7361  Basecbs 17141  lecple 17189  occoc 17190  joincjn 18239  meetcmee 18240  HLchlt 39689  LHypclh 40323  LTrncltrn 40440  DIsoAcdia 41367  ocAcocaN 41458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-riotaBAD 39292

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-iun 4949  df-iin 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-undef 8218  df-map 8770  df-proset 18222  df-poset 18241  df-plt 18256  df-lub 18272  df-glb 18273  df-join 18274  df-meet 18275  df-p0 18351  df-p1 18352  df-lat 18360  df-clat 18427  df-oposet 39515  df-ol 39517  df-oml 39518  df-covers 39605  df-ats 39606  df-atl 39637  df-cvlat 39661  df-hlat 39690  df-llines 39837  df-lplanes 39838  df-lvols 39839  df-lines 39840  df-psubsp 39842  df-pmap 39843  df-padd 40135  df-lhyp 40327  df-laut 40328  df-ldil 40443  df-ltrn 40444  df-trl 40498  df-disoa 41368  df-docaN 41459

This theorem is referenced by:  doca2N  41465  djajN  41476