dihjust

Description: Part of proof after Lemma N of Crawley p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014)

	Ref	Expression
Hypotheses	dihjust.b	$⊢ B = {Base}_{K}$
	dihjust.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihjust.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihjust.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihjust.a	$⊢ A = Atoms (K)$
	dihjust.h	$⊢ H = LHyp (K)$
	dihjust.i	$⊢ I = DIsoB (K) (W)$
	dihjust.J	$⊢ J = DIsoC (K) (W)$
	dihjust.u	$⊢ U = DVecH (K) (W)$
	dihjust.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	dihjust	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) = J (R) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		dihjust.b	$⊢ B = {Base}_{K}$
2		dihjust.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihjust.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihjust.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihjust.a	$⊢ A = Atoms (K)$
6		dihjust.h	$⊢ H = LHyp (K)$
7		dihjust.i	$⊢ I = DIsoB (K) (W)$
8		dihjust.J	$⊢ J = DIsoC (K) (W)$
9		dihjust.u	$⊢ U = DVecH (K) (W)$
10		dihjust.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
11	1 2 3 4 5 6 7 8 9 10	dihjustlem	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (R) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$
12		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to (K \in HL \land W \in H)$
13		simp22	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
14		simp21	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
15		simp23	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to X \in B$
16		simp3	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)$
17	16	eqcomd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to R \underset{˙}{\lor} (X \underset{˙}{\land} W) = Q \underset{˙}{\lor} (X \underset{˙}{\land} W)$
18	1 2 3 4 5 6 7 8 9 10	dihjustlem	$⊢ ((K \in HL \land W \in H) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land X \in B) \land R \underset{˙}{\lor} (X \underset{˙}{\land} W) = Q \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to J (R) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$
19	12 13 14 15 17 18	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to J (R) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$
20	11 19	eqssd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land X \in B) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = R \underset{˙}{\lor} (X \underset{˙}{\land} W)) \to J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) = J (R) \underset{˙}{\oplus} I (X \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihjust

Proof