cdlemn4a

Description: Part of proof of Lemma N of Crawley p. 121 line 32. (Contributed by NM, 24-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn4.b	$⊢ B = {Base}_{K}$
	cdlemn4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn4.a	$⊢ A = Atoms (K)$
	cdlemn4.p	$⊢ P = oc (K) (W)$
	cdlemn4.h	$⊢ H = LHyp (K)$
	cdlemn4.t	$⊢ T = LTrn (K) (W)$
	cdlemn4.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	cdlemn4.u	$⊢ U = DVecH (K) (W)$
	cdlemn4.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	cdlemn4.g	$⊢ G = (ι h \in T \| h (P) = R)$
	cdlemn4.j	$⊢ J = (ι h \in T \| h (Q) = R)$
	cdlemn4a.n	$⊢ N = LSpan (U)$
	cdlemn4a.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	cdlemn4a	$⊢ ((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)) \to N (\{⟨G, {I ↾}_{T}⟩\}) \subseteq N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨J, O⟩\})$

Proof

Step	Hyp	Ref	Expression
1		cdlemn4.b	$⊢ B = {Base}_{K}$
2		cdlemn4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn4.a	$⊢ A = Atoms (K)$
4		cdlemn4.p	$⊢ P = oc (K) (W)$
5		cdlemn4.h	$⊢ H = LHyp (K)$
6		cdlemn4.t	$⊢ T = LTrn (K) (W)$
7		cdlemn4.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
8		cdlemn4.u	$⊢ U = DVecH (K) (W)$
9		cdlemn4.f	$⊢ F = (ι h \in T \| h (P) = Q)$
10		cdlemn4.g	$⊢ G = (ι h \in T \| h (P) = R)$
11		cdlemn4.j	$⊢ J = (ι h \in T \| h (Q) = R)$
12		cdlemn4a.n	$⊢ N = LSpan (U)$
13		cdlemn4a.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
14		eqid	$⊢ +_{U} = +_{U}$
15	1 2 3 4 5 6 7 8 9 10 11 14	cdlemn4	$⊢ ((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)) \to ⟨G, {I ↾}_{T}⟩ = ⟨F, {I ↾}_{T}⟩ +_{U} ⟨J, O⟩$
16	15	sneqd	$⊢ ((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)) \to \{⟨G, {I ↾}_{T}⟩\} = \{⟨F, {I ↾}_{T}⟩ +_{U} ⟨J, O⟩\}$
17	16	fveq2d	$⊢ ((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)) \to N (\{⟨G, {I ↾}_{T}⟩\}) = N (\{⟨F, {I ↾}_{T}⟩ +_{U} ⟨J, O⟩\})$
18		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)) \to (K \in HL \land W \in H)$
19	5 8 18	dvhlmod	$⊢ ((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)) \to U \in LMod$
20	2 3 5 4	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21	20	3ad2ant1	$⊢ ((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)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
22		simp2	$⊢ ((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)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
23	2 3 5 6 9	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
24	18 21 22 23	syl3anc	$⊢ ((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)) \to F \in T$
25		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
26	5 6 25	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in TEndo (K) (W)$
27	26	3ad2ant1	$⊢ ((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)) \to {I ↾}_{T} \in TEndo (K) (W)$
28		eqid	$⊢ {Base}_{U} = {Base}_{U}$
29	5 6 25 8 28	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (F \in T \land {I ↾}_{T} \in TEndo (K) (W))) \to ⟨F, {I ↾}_{T}⟩ \in {Base}_{U}$
30	18 24 27 29	syl12anc	$⊢ ((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)) \to ⟨F, {I ↾}_{T}⟩ \in {Base}_{U}$
31	2 3 5 6 11	ltrniotacl	$⊢ ((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)) \to J \in T$
32	1 5 6 25 7	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in TEndo (K) (W)$
33	32	3ad2ant1	$⊢ ((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)) \to O \in TEndo (K) (W)$
34	5 6 25 8 28	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (J \in T \land O \in TEndo (K) (W))) \to ⟨J, O⟩ \in {Base}_{U}$
35	18 31 33 34	syl12anc	$⊢ ((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)) \to ⟨J, O⟩ \in {Base}_{U}$
36	28 14 12 13	lspsntri	$⊢ (U \in LMod \land ⟨F, {I ↾}_{T}⟩ \in {Base}_{U} \land ⟨J, O⟩ \in {Base}_{U}) \to N (\{⟨F, {I ↾}_{T}⟩ +_{U} ⟨J, O⟩\}) \subseteq N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨J, O⟩\})$
37	19 30 35 36	syl3anc	$⊢ ((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)) \to N (\{⟨F, {I ↾}_{T}⟩ +_{U} ⟨J, O⟩\}) \subseteq N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨J, O⟩\})$
38	17 37	eqsstrd	$⊢ ((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)) \to N (\{⟨G, {I ↾}_{T}⟩\}) \subseteq N (\{⟨F, {I ↾}_{T}⟩\}) \underset{˙}{\oplus} N (\{⟨J, O⟩\})$

Metamath Proof Explorer

Theorem cdlemn4a

Proof