cdlemn11a

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

	Ref	Expression
Hypotheses	cdlemn11a.b	$⊢ B = {Base}_{K}$
	cdlemn11a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn11a.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemn11a.a	$⊢ A = Atoms (K)$
	cdlemn11a.h	$⊢ H = LHyp (K)$
	cdlemn11a.p	$⊢ P = oc (K) (W)$
	cdlemn11a.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	cdlemn11a.t	$⊢ T = LTrn (K) (W)$
	cdlemn11a.r	$⊢ R = trL (K) (W)$
	cdlemn11a.e	$⊢ E = TEndo (K) (W)$
	cdlemn11a.i	$⊢ I = DIsoB (K) (W)$
	cdlemn11a.J	$⊢ J = DIsoC (K) (W)$
	cdlemn11a.u	$⊢ U = DVecH (K) (W)$
	cdlemn11a.d	$⊢ \underset{˙}{+} = +_{U}$
	cdlemn11a.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	cdlemn11a.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	cdlemn11a.g	$⊢ G = (ι h \in T \| h (P) = N)$
Assertion	cdlemn11a	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to ⟨G, {I ↾}_{T}⟩ \in J (N)$

Proof

Step	Hyp	Ref	Expression
1		cdlemn11a.b	$⊢ B = {Base}_{K}$
2		cdlemn11a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn11a.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemn11a.a	$⊢ A = Atoms (K)$
5		cdlemn11a.h	$⊢ H = LHyp (K)$
6		cdlemn11a.p	$⊢ P = oc (K) (W)$
7		cdlemn11a.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
8		cdlemn11a.t	$⊢ T = LTrn (K) (W)$
9		cdlemn11a.r	$⊢ R = trL (K) (W)$
10		cdlemn11a.e	$⊢ E = TEndo (K) (W)$
11		cdlemn11a.i	$⊢ I = DIsoB (K) (W)$
12		cdlemn11a.J	$⊢ J = DIsoC (K) (W)$
13		cdlemn11a.u	$⊢ U = DVecH (K) (W)$
14		cdlemn11a.d	$⊢ \underset{˙}{+} = +_{U}$
15		cdlemn11a.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
16		cdlemn11a.f	$⊢ F = (ι h \in T \| h (P) = Q)$
17		cdlemn11a.g	$⊢ G = (ι h \in T \| h (P) = N)$
18		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (K \in HL \land W \in H)$
19	2 4 5 6	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
20	19	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21		simp22	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (N \in A \land \neg N \underset{˙}{\leq} W)$
22	2 4 5 8 17	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \to G \in T$
23	18 20 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to G \in T$
24		fvresi	$⊢ G \in T \to ({I ↾}_{T}) (G) = G$
25	23 24	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to ({I ↾}_{T}) (G) = G$
26	25	eqcomd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to G = ({I ↾}_{T}) (G)$
27	5 8 10	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
28	27	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to {I ↾}_{T} \in E$
29		riotaex	$⊢ (ι h \in T \| h (P) = N) \in V$
30	17 29	eqeltri	$⊢ G \in V$
31	8	fvexi	$⊢ T \in V$
32		resiexg	$⊢ T \in V \to {I ↾}_{T} \in V$
33	31 32	ax-mp	$⊢ {I ↾}_{T} \in V$
34	2 4 5 6 8 10 12 17 30 33	dicopelval2	$⊢ ((K \in HL \land W \in H) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \to (⟨G, {I ↾}_{T}⟩ \in J (N) \leftrightarrow (G = ({I ↾}_{T}) (G) \land {I ↾}_{T} \in E))$
35	18 21 34	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to (⟨G, {I ↾}_{T}⟩ \in J (N) \leftrightarrow (G = ({I ↾}_{T}) (G) \land {I ↾}_{T} \in E))$
36	26 28 35	mpbir2and	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land J (N) \subseteq J (Q) \underset{˙}{\oplus} I (X)) \to ⟨G, {I ↾}_{T}⟩ \in J (N)$

Metamath Proof Explorer

Theorem cdlemn11a

Proof