ltrnj

Description: Lattice translation of a meet. TODO: change antecedent to K e. HL (Contributed by NM, 25-May-2012)

	Ref	Expression
Hypotheses	ltrnj.b	$⊢ B = {Base}_{K}$
	ltrnj.j	$⊢ \underset{˙}{\lor} = join (K)$
	ltrnj.h	$⊢ H = LHyp (K)$
	ltrnj.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnj	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{\lor} F (Y)$

Step	Hyp	Ref	Expression
1		ltrnj.b	$⊢ B = {Base}_{K}$
2		ltrnj.j	$⊢ \underset{˙}{\lor} = join (K)$
3		ltrnj.h	$⊢ H = LHyp (K)$
4		ltrnj.t	$⊢ T = LTrn (K) (W)$
5		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to K \in HL$
6	5	hllatd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to K \in Lat$
7		eqid	$⊢ LAut (K) = LAut (K)$
8	3 7 4	ltrnlaut	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in LAut (K)$
9	8	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to F \in LAut (K)$
10		simp3l	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to X \in B$
11		simp3r	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to Y \in B$
12	1 2 7	lautj	$⊢ (K \in Lat \land (F \in LAut (K) \land X \in B \land Y \in B)) \to F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{\lor} F (Y)$
13	6 9 10 11 12	syl13anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{\lor} F (Y)$

Metamath Proof Explorer