cdlemn7

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

	Ref	Expression
Hypotheses	cdlemn8.b	$⊢ B = {Base}_{K}$
	cdlemn8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn8.a	$⊢ A = Atoms (K)$
	cdlemn8.h	$⊢ H = LHyp (K)$
	cdlemn8.p	$⊢ P = oc (K) (W)$
	cdlemn8.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	cdlemn8.t	$⊢ T = LTrn (K) (W)$
	cdlemn8.e	$⊢ E = TEndo (K) (W)$
	cdlemn8.u	$⊢ U = DVecH (K) (W)$
	cdlemn8.s	$⊢ \underset{˙}{+} = +_{U}$
	cdlemn8.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	cdlemn8.g	$⊢ G = (ι h \in T \| h (P) = R)$
Assertion	cdlemn7	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (G = s (F) \circ g \land {I ↾}_{T} = s)$

Proof

Step	Hyp	Ref	Expression
1		cdlemn8.b	$⊢ B = {Base}_{K}$
2		cdlemn8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn8.a	$⊢ A = Atoms (K)$
4		cdlemn8.h	$⊢ H = LHyp (K)$
5		cdlemn8.p	$⊢ P = oc (K) (W)$
6		cdlemn8.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
7		cdlemn8.t	$⊢ T = LTrn (K) (W)$
8		cdlemn8.e	$⊢ E = TEndo (K) (W)$
9		cdlemn8.u	$⊢ U = DVecH (K) (W)$
10		cdlemn8.s	$⊢ \underset{˙}{+} = +_{U}$
11		cdlemn8.f	$⊢ F = (ι h \in T \| h (P) = Q)$
12		cdlemn8.g	$⊢ G = (ι h \in T \| h (P) = R)$
13		simp33	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩$
14		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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (K \in HL \land W \in H)$
15		simp2l	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
16		simp2r	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
17		simp31	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to s \in E$
18		simp32	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to g \in T$
19	1 2 3 4 5 6 7 8 9 10 11	cdlemn6	$⊢ ((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)) \land (s \in E \land g \in T)) \to ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (F) \circ g, s⟩$
20	14 15 16 17 18 19	syl122anc	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (F) \circ g, s⟩$
21	13 20	eqtrd	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ⟨G, {I ↾}_{T}⟩ = ⟨s (F) \circ g, s⟩$
22		fvex	$⊢ s (F) \in V$
23		vex	$⊢ g \in V$
24	22 23	coex	$⊢ s (F) \circ g \in V$
25		vex	$⊢ s \in V$
26	24 25	opth2	$⊢ ⟨G, {I ↾}_{T}⟩ = ⟨s (F) \circ g, s⟩ \leftrightarrow (G = s (F) \circ g \land {I ↾}_{T} = s)$
27	21 26	sylib	$⊢ ((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)) \land (s \in E \land g \in T \land ⟨G, {I ↾}_{T}⟩ = ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (G = s (F) \circ g \land {I ↾}_{T} = s)$

Metamath Proof Explorer

Theorem cdlemn7

Proof