dia2dim

Description: A two-dimensional subspace of partial vector space A is closed, or equivalently, the isomorphism of a join of two atoms is a subset of the subspace sum of the isomorphisms of each atom (and thus they are equal, as shown later for the full vector space H). (Contributed by NM, 9-Sep-2014)

	Ref	Expression
Hypotheses	dia2dim.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dia2dim.j	$⊢ \underset{˙}{\lor} = join (K)$
	dia2dim.a	$⊢ A = Atoms (K)$
	dia2dim.h	$⊢ H = LHyp (K)$
	dia2dim.y	$⊢ Y = DVecA (K) (W)$
	dia2dim.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
	dia2dim.i	$⊢ I = DIsoA (K) (W)$
	dia2dim.k	$⊢ φ \to (K \in HL \land W \in H)$
	dia2dim.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
	dia2dim.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
Assertion	dia2dim	$⊢ φ \to I (U \underset{˙}{\lor} V) \subseteq I (U) \underset{˙}{\oplus} I (V)$

Proof

Step	Hyp	Ref	Expression
1		dia2dim.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dim.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dia2dim.a	$⊢ A = Atoms (K)$
4		dia2dim.h	$⊢ H = LHyp (K)$
5		dia2dim.y	$⊢ Y = DVecA (K) (W)$
6		dia2dim.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
7		dia2dim.i	$⊢ I = DIsoA (K) (W)$
8		dia2dim.k	$⊢ φ \to (K \in HL \land W \in H)$
9		dia2dim.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
10		dia2dim.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
11		eqid	$⊢ meet (K) = meet (K)$
12		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
13		eqid	$⊢ trL (K) (W) = trL (K) (W)$
14		eqid	$⊢ LSubSp (Y) = LSubSp (Y)$
15		eqid	$⊢ LSpan (Y) = LSpan (Y)$
16	1 2 11 3 4 12 13 5 14 6 15 7 8 9 10	dia2dimlem13	$⊢ φ \to I (U \underset{˙}{\lor} V) \subseteq I (U) \underset{˙}{\oplus} I (V)$

Metamath Proof Explorer

Theorem dia2dim

Proof