lcfrlem18

	Ref	Expression
Hypotheses	lcfrlem17.h	$⊢ H = LHyp (K)$
	lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem17.u	$⊢ U = DVecH (K) (W)$
	lcfrlem17.v	$⊢ V = {Base}_{U}$
	lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfrlem17.n	$⊢ N = LSpan (U)$
	lcfrlem17.a	$⊢ A = LSAtoms (U)$
	lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
Assertion	lcfrlem18	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$

Step	Hyp	Ref	Expression
1		lcfrlem17.h	$⊢ H = LHyp (K)$
2		lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem17.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem17.v	$⊢ V = {Base}_{U}$
5		lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
6		lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
7		lcfrlem17.n	$⊢ N = LSpan (U)$
8		lcfrlem17.a	$⊢ A = LSAtoms (U)$
9		lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
11		lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
12		lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
13		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
14	13	fveq2i	$⊢ \underset{˙}{⊥} (\{X, Y\}) = \underset{˙}{⊥} (\{X\} \cup \{Y\})$
15	10	eldifad	$⊢ φ \to X \in V$
16	15	snssd	$⊢ φ \to \{X\} \subseteq V$
17	11	eldifad	$⊢ φ \to Y \in V$
18	17	snssd	$⊢ φ \to \{Y\} \subseteq V$
19	1 3 4 2	dochdmj1	$⊢ ((K \in HL \land W \in H) \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to \underset{˙}{⊥} (\{X\} \cup \{Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
20	9 16 18 19	syl3anc	$⊢ φ \to \underset{˙}{⊥} (\{X\} \cup \{Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$
21	14 20	eqtrid	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) = \underset{˙}{⊥} (\{X\}) \cap \underset{˙}{⊥} (\{Y\})$

Metamath Proof Explorer