lss0v

Description: The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015)

	Ref	Expression
Hypotheses	lss0v.x	$⊢ X = W ↾_{𝑠} U$
	lss0v.o	$⊢ \underset{˙}{0} = 0_{W}$
	lss0v.z	$⊢ Z = 0_{X}$
	lss0v.l	$⊢ L = LSubSp (W)$
Assertion	lss0v	$⊢ (W \in LMod \land U \in L) \to Z = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		lss0v.x	$⊢ X = W ↾_{𝑠} U$
2		lss0v.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lss0v.z	$⊢ Z = 0_{X}$
4		lss0v.l	$⊢ L = LSubSp (W)$
5		0ss	$⊢ \emptyset \subseteq U$
6		eqid	$⊢ LSpan (W) = LSpan (W)$
7		eqid	$⊢ LSpan (X) = LSpan (X)$
8	1 6 7 4	lsslsp	$⊢ (W \in LMod \land U \in L \land \emptyset \subseteq U) \to LSpan (W) (\emptyset) = LSpan (X) (\emptyset)$
9	5 8	mp3an3	$⊢ (W \in LMod \land U \in L) \to LSpan (W) (\emptyset) = LSpan (X) (\emptyset)$
10	2 6	lsp0	$⊢ W \in LMod \to LSpan (W) (\emptyset) = \{\underset{˙}{0}\}$
11	10	adantr	$⊢ (W \in LMod \land U \in L) \to LSpan (W) (\emptyset) = \{\underset{˙}{0}\}$
12	1 4	lsslmod	$⊢ (W \in LMod \land U \in L) \to X \in LMod$
13	3 7	lsp0	$⊢ X \in LMod \to LSpan (X) (\emptyset) = \{Z\}$
14	12 13	syl	$⊢ (W \in LMod \land U \in L) \to LSpan (X) (\emptyset) = \{Z\}$
15	9 11 14	3eqtr3rd	$⊢ (W \in LMod \land U \in L) \to \{Z\} = \{\underset{˙}{0}\}$
16	15	unieqd	$⊢ (W \in LMod \land U \in L) \to ⋃ \{Z\} = ⋃ \{\underset{˙}{0}\}$
17	3	fvexi	$⊢ Z \in V$
18	17	unisn	$⊢ ⋃ \{Z\} = Z$
19	2	fvexi	$⊢ \underset{˙}{0} \in V$
20	19	unisn	$⊢ ⋃ \{\underset{˙}{0}\} = \underset{˙}{0}$
21	16 18 20	3eqtr3g	$⊢ (W \in LMod \land U \in L) \to Z = \underset{˙}{0}$

Metamath Proof Explorer