diaocN

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

	Ref	Expression
Hypotheses	diaoc.j	$⊢ \underset{˙}{\lor} = join (K)$
	diaoc.m	$⊢ \underset{˙}{\land} = meet (K)$
	diaoc.o	$⊢ \underset{˙}{⊥} = oc (K)$
	diaoc.h	$⊢ H = LHyp (K)$
	diaoc.t	$⊢ T = LTrn (K) (W)$
	diaoc.i	$⊢ I = DIsoA (K) (W)$
	diaoc.n	$⊢ N = ocA (K) (W)$
Assertion	diaocN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I ((\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (W)) \underset{˙}{\land} W) = N (I (X))$

Proof

Step	Hyp	Ref	Expression
1		diaoc.j	$⊢ \underset{˙}{\lor} = join (K)$
2		diaoc.m	$⊢ \underset{˙}{\land} = meet (K)$
3		diaoc.o	$⊢ \underset{˙}{⊥} = oc (K)$
4		diaoc.h	$⊢ H = LHyp (K)$
5		diaoc.t	$⊢ T = LTrn (K) (W)$
6		diaoc.i	$⊢ I = DIsoA (K) (W)$
7		diaoc.n	$⊢ N = ocA (K) (W)$
8		simpl	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to (K \in HL \land W \in H)$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 4 6	diadmclN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to X \in {Base}_{K}$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12	11 4 6	diadmleN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to X \leq_{K} W$
13	9 11 4 5 6	diass	$⊢ ((K \in HL \land W \in H) \land (X \in {Base}_{K} \land X \leq_{K} W)) \to I (X) \subseteq T$
14	8 10 12 13	syl12anc	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I (X) \subseteq T$
15	1 2 3 4 5 6 7	docavalN	$⊢ ((K \in HL \land W \in H) \land I (X) \subseteq T) \to N (I (X)) = I ((\underset{˙}{⊥} (I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (W)) \underset{˙}{\land} W)$
16	14 15	syldan	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to N (I (X)) = I ((\underset{˙}{⊥} (I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (W)) \underset{˙}{\land} W)$
17	4 6	diaclN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I (X) \in ran I$
18		intmin	$⊢ I (X) \in ran I \to ⋂ \{z \in ran I \| I (X) \subseteq z\} = I (X)$
19	17 18	syl	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to ⋂ \{z \in ran I \| I (X) \subseteq z\} = I (X)$
20	19	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\}) = I^{-1} (I (X))$
21	4 6	diaf11N	$⊢ (K \in HL \land W \in H) \to I : dom I \underset{1-1 onto}{⟶} ran I$
22		f1ocnvfv1	$⊢ (I : dom I \underset{1-1 onto}{⟶} ran I \land X \in dom I) \to I^{-1} (I (X)) = X$
23	21 22	sylan	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I^{-1} (I (X)) = X$
24	20 23	eqtrd	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\}) = X$
25	24	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to \underset{˙}{⊥} (I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\})) = \underset{˙}{⊥} (X)$
26	25	oveq1d	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to \underset{˙}{⊥} (I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (W) = \underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (W)$
27	26	fvoveq1d	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I ((\underset{˙}{⊥} (I^{-1} (⋂ \{z \in ran I \| I (X) \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (W)) \underset{˙}{\land} W) = I ((\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (W)) \underset{˙}{\land} W)$
28	16 27	eqtr2d	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I ((\underset{˙}{⊥} (X) \underset{˙}{\lor} \underset{˙}{⊥} (W)) \underset{˙}{\land} W) = N (I (X))$

Metamath Proof Explorer

Theorem diaocN

Proof