llnexch2N

Description: Line exchange property (compare cvlatexch2 for atoms). (Contributed by NM, 18-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	llnexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llnexch.j	$⊢ \underset{˙}{\lor} = join (K)$
	llnexch.m	$⊢ \underset{˙}{\land} = meet (K)$
	llnexch.a	$⊢ A = Atoms (K)$
	llnexch.n	$⊢ N = LLines (K)$
Assertion	llnexch2N	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$

Proof

Step	Hyp	Ref	Expression
1		llnexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llnexch.j	$⊢ \underset{˙}{\lor} = join (K)$
3		llnexch.m	$⊢ \underset{˙}{\land} = meet (K)$
4		llnexch.a	$⊢ A = Atoms (K)$
5		llnexch.n	$⊢ N = LLines (K)$
6	1 2 3 4 5	llnexchb2	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)$
7		hllat	$⊢ K \in HL \to K \in Lat$
8	7	3ad2ant1	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to K \in Lat$
9		simp21	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to X \in N$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 5	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
12	9 11	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to X \in {Base}_{K}$
13		simp22	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to Y \in N$
14	10 5	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
15	13 14	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to Y \in {Base}_{K}$
16	10 1 3	latmle2	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
17	8 12 15 16	syl3anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
18		breq1	$⊢ X \underset{˙}{\land} Y = X \underset{˙}{\land} Z \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Y \leftrightarrow (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$
19	17 18	syl5ibcom	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to (X \underset{˙}{\land} Y = X \underset{˙}{\land} Z \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$
20	6 19	sylbid	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \to (X \underset{˙}{\land} Z) \underset{˙}{\leq} Y)$

Metamath Proof Explorer

Theorem llnexch2N

Proof