cdlemn4

Description: Part of proof of Lemma N of Crawley p. 121 line 31. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 24-Jun-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)$
	cdlemn4.s	$⊢ \underset{˙}{+} = +_{U}$
Assertion	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}⟩ \underset{˙}{+} ⟨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		cdlemn4.s	$⊢ \underset{˙}{+} = +_{U}$
13		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)$
14	2 3 5 4	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
15	13 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)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
16		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)$
17	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$
18	13 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)) \to F \in T$
19		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
20	5 6 19	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in TEndo (K) (W)$
21	13 20	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)) \to {I ↾}_{T} \in TEndo (K) (W)$
22	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$
23	1 5 6 19 7	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in TEndo (K) (W)$
24	13 23	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)) \to O \in TEndo (K) (W)$
25		eqid	$⊢ Scalar (U) = Scalar (U)$
26		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
27	5 6 19 8 25 12 26	dvhopvadd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land {I ↾}_{T} \in TEndo (K) (W)) \land (J \in T \land O \in TEndo (K) (W))) \to ⟨F, {I ↾}_{T}⟩ \underset{˙}{+} ⟨J, O⟩ = ⟨F \circ J, ({I ↾}_{T}) +_{Scalar (U)} O⟩$
28	13 18 21 22 24 27	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)) \to ⟨F, {I ↾}_{T}⟩ \underset{˙}{+} ⟨J, O⟩ = ⟨F \circ J, ({I ↾}_{T}) +_{Scalar (U)} O⟩$
29	5 6	ltrncom	$⊢ ((K \in HL \land W \in H) \land F \in T \land J \in T) \to F \circ J = J \circ F$
30	13 18 22 29	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 \circ J = J \circ F$
31	2 3 4 5 6 9 10 11	cdlemn3	$⊢ ((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 \circ F = G$
32	30 31	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)) \to F \circ J = G$
33		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
34	5 33 8 25	dvhsca	$⊢ (K \in HL \land W \in H) \to Scalar (U) = EDRing (K) (W)$
35	34	fveq2d	$⊢ (K \in HL \land W \in H) \to 0_{Scalar (U)} = 0_{EDRing (K) (W)}$
36		eqid	$⊢ 0_{EDRing (K) (W)} = 0_{EDRing (K) (W)}$
37	1 5 6 33 7 36	erng0g	$⊢ (K \in HL \land W \in H) \to 0_{EDRing (K) (W)} = O$
38	35 37	eqtrd	$⊢ (K \in HL \land W \in H) \to 0_{Scalar (U)} = O$
39	13 38	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)) \to 0_{Scalar (U)} = O$
40	39	oveq2d	$⊢ ((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}) +_{Scalar (U)} 0_{Scalar (U)} = ({I ↾}_{T}) +_{Scalar (U)} O$
41	5 33	erngdv	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in DivRing$
42		drnggrp	$⊢ EDRing (K) (W) \in DivRing \to EDRing (K) (W) \in Grp$
43	41 42	syl	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in Grp$
44	34 43	eqeltrd	$⊢ (K \in HL \land W \in H) \to Scalar (U) \in Grp$
45	13 44	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)) \to Scalar (U) \in Grp$
46		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
47	5 19 8 25 46	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
48	13 47	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)) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
49	21 48	eleqtrrd	$⊢ ((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 {Base}_{Scalar (U)}$
50		eqid	$⊢ 0_{Scalar (U)} = 0_{Scalar (U)}$
51	46 26 50	grprid	$⊢ (Scalar (U) \in Grp \land {I ↾}_{T} \in {Base}_{Scalar (U)}) \to ({I ↾}_{T}) +_{Scalar (U)} 0_{Scalar (U)} = {I ↾}_{T}$
52	45 49 51	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)) \to ({I ↾}_{T}) +_{Scalar (U)} 0_{Scalar (U)} = {I ↾}_{T}$
53	40 52	eqtr3d	$⊢ ((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}) +_{Scalar (U)} O = {I ↾}_{T}$
54	32 53	opeq12d	$⊢ ((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 \circ J, ({I ↾}_{T}) +_{Scalar (U)} O⟩ = ⟨G, {I ↾}_{T}⟩$
55	28 54	eqtr2d	$⊢ ((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}⟩ \underset{˙}{+} ⟨J, O⟩$

Metamath Proof Explorer

Theorem cdlemn4

Proof