lnjatN

Description: Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnjat.b	$⊢ B = {Base}_{K}$
	lnjat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lnjat.j	$⊢ \underset{˙}{\lor} = join (K)$
	lnjat.a	$⊢ A = Atoms (K)$
	lnjat.n	$⊢ N = Lines (K)$
	lnjat.m	$⊢ M = pmap (K)$
Assertion	lnjatN	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to \exists q \in A (q \neq P \land X = P \underset{˙}{\lor} q)$

Proof

Step	Hyp	Ref	Expression
1		lnjat.b	$⊢ B = {Base}_{K}$
2		lnjat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lnjat.j	$⊢ \underset{˙}{\lor} = join (K)$
4		lnjat.a	$⊢ A = Atoms (K)$
5		lnjat.n	$⊢ N = Lines (K)$
6		lnjat.m	$⊢ M = pmap (K)$
7		simpl1	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to K \in HL$
8		simpl2	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to X \in B$
9		simprl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to M (X) \in N$
10	1 2 4 5 6	lnatexN	$⊢ (K \in HL \land X \in B \land M (X) \in N) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to \exists q \in A (q \neq P \land q \underset{˙}{\leq} X)$
12		simp3l	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to q \neq P$
13		simp1l1	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to K \in HL$
14		simp1l2	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to X \in B$
15		simp1rl	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to M (X) \in N$
16		simp1l3	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to P \in A$
17		simp2	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to q \in A$
18	12	necomd	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to P \neq q$
19		simp1rr	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to P \underset{˙}{\leq} X$
20		simp3r	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to q \underset{˙}{\leq} X$
21	1 2 3 4 5 6	lneq2at	$⊢ ((K \in HL \land X \in B \land M (X) \in N) \land (P \in A \land q \in A \land P \neq q) \land (P \underset{˙}{\leq} X \land q \underset{˙}{\leq} X)) \to X = P \underset{˙}{\lor} q$
22	13 14 15 16 17 18 19 20 21	syl332anc	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to X = P \underset{˙}{\lor} q$
23	12 22	jca	$⊢ (((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \land q \in A \land (q \neq P \land q \underset{˙}{\leq} X)) \to (q \neq P \land X = P \underset{˙}{\lor} q)$
24	23	3exp	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to (q \in A \to ((q \neq P \land q \underset{˙}{\leq} X) \to (q \neq P \land X = P \underset{˙}{\lor} q)))$
25	24	reximdvai	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to (\exists q \in A (q \neq P \land q \underset{˙}{\leq} X) \to \exists q \in A (q \neq P \land X = P \underset{˙}{\lor} q))$
26	11 25	mpd	$⊢ ((K \in HL \land X \in B \land P \in A) \land (M (X) \in N \land P \underset{˙}{\leq} X)) \to \exists q \in A (q \neq P \land X = P \underset{˙}{\lor} q)$

Metamath Proof Explorer

Theorem lnjatN

Proof