cdlemn6

Description: Part of proof of Lemma N of Crawley p. 121 line 35. (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)$
Assertion	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⟩$

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		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)) \to (K \in HL \land W \in H)$
13		simp3l	$⊢ ((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 \in E$
14	2 3 4 5	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
15	12 14	syl	$⊢ ((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 (P \in A \land \neg P \underset{˙}{\leq} W)$
16		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)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
17	2 3 4 7 11	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$
18	12 15 16 17	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)) \land (s \in E \land g \in T)) \to F \in T$
19	4 7 8	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land F \in T) \to s (F) \in T$
20	12 13 18 19	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)) \land (s \in E \land g \in T)) \to s (F) \in T$
21		simp3r	$⊢ ((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 g \in T$
22	1 4 7 8 6	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
23	12 22	syl	$⊢ ((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 O \in E$
24		eqid	$⊢ Scalar (U) = Scalar (U)$
25		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
26	4 7 8 9 24 10 25	dvhopvadd	$⊢ ((K \in HL \land W \in H) \land (s (F) \in T \land s \in E) \land (g \in T \land O \in E)) \to ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (F) \circ g, s +_{Scalar (U)} O⟩$
27	12 20 13 21 23 26	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)) \to ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (F) \circ g, s +_{Scalar (U)} O⟩$
28		eqid	$⊢ (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h))) = (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h)))$
29	4 7 8 9 24 28 25	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h)))$
30	12 29	syl	$⊢ ((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 +_{Scalar (U)} = (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h)))$
31	30	oveqd	$⊢ ((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 +_{Scalar (U)} O = s (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h))) O$
32	1 4 7 8 6 28	tendo0plr	$⊢ ((K \in HL \land W \in H) \land s \in E) \to s (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h))) O = s$
33	12 13 32	syl2anc	$⊢ ((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 (t \in E, u \in E ⟼ (h \in T ⟼ t (h) \circ u (h))) O = s$
34	31 33	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)) \to s +_{Scalar (U)} O = s$
35	34	opeq2d	$⊢ ((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) \circ g, s +_{Scalar (U)} O⟩ = ⟨s (F) \circ g, s⟩$
36	27 35	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)) \to ⟨s (F), s⟩ \underset{˙}{+} ⟨g, O⟩ = ⟨s (F) \circ g, s⟩$

Metamath Proof Explorer

Theorem cdlemn6

Proof