dicvaddcl

Description: Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014)

	Ref	Expression
Hypotheses	dicvaddcl.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicvaddcl.a	$⊢ A = Atoms (K)$
	dicvaddcl.h	$⊢ H = LHyp (K)$
	dicvaddcl.u	$⊢ U = DVecH (K) (W)$
	dicvaddcl.i	$⊢ I = DIsoC (K) (W)$
	dicvaddcl.p	$⊢ \underset{˙}{+} = +_{U}$
Assertion	dicvaddcl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to X \underset{˙}{+} Y \in I (Q)$

Proof

Step	Hyp	Ref	Expression
1		dicvaddcl.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicvaddcl.a	$⊢ A = Atoms (K)$
3		dicvaddcl.h	$⊢ H = LHyp (K)$
4		dicvaddcl.u	$⊢ U = DVecH (K) (W)$
5		dicvaddcl.i	$⊢ I = DIsoC (K) (W)$
6		dicvaddcl.p	$⊢ \underset{˙}{+} = +_{U}$
7		simp1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (K \in HL \land W \in H)$
8		eqid	$⊢ {Base}_{U} = {Base}_{U}$
9	1 2 3 5 4 8	dicssdvh	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq {Base}_{U}$
10		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
11		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
12	3 10 11 4 8	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = LTrn (K) (W) \times TEndo (K) (W)$
13	12	eqcomd	$⊢ (K \in HL \land W \in H) \to LTrn (K) (W) \times TEndo (K) (W) = {Base}_{U}$
14	13	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to LTrn (K) (W) \times TEndo (K) (W) = {Base}_{U}$
15	9 14	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq LTrn (K) (W) \times TEndo (K) (W)$
16	15	3adant3	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to I (Q) \subseteq LTrn (K) (W) \times TEndo (K) (W)$
17		simp3l	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to X \in I (Q)$
18	16 17	sseldd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to X \in (LTrn (K) (W) \times TEndo (K) (W))$
19		simp3r	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to Y \in I (Q)$
20	16 19	sseldd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to Y \in (LTrn (K) (W) \times TEndo (K) (W))$
21		eqid	$⊢ Scalar (U) = Scalar (U)$
22		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
23	3 10 11 4 21 6 22	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (X \in (LTrn (K) (W) \times TEndo (K) (W)) \land Y \in (LTrn (K) (W) \times TEndo (K) (W)))) \to X \underset{˙}{+} Y = ⟨1^{st} (X) \circ 1^{st} (Y), 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)⟩$
24	7 18 20 23	syl12anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to X \underset{˙}{+} Y = ⟨1^{st} (X) \circ 1^{st} (Y), 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)⟩$
25	1 2 3 11 5	dicelval2nd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land X \in I (Q)) \to 2^{nd} (X) \in TEndo (K) (W)$
26	25	3adant3r	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 2^{nd} (X) \in TEndo (K) (W)$
27	1 2 3 11 5	dicelval2nd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 2^{nd} (Y) \in TEndo (K) (W)$
28	27	3adant3l	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 2^{nd} (Y) \in TEndo (K) (W)$
29		eqid	$⊢ oc (K) = oc (K)$
30	1 29 2 3	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
31	30	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
32		simp2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
33		eqid	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) = (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)$
34	1 2 3 10 33	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
35	7 31 32 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
36		eqid	$⊢ (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h)))$
37	10 36	tendospdi2	$⊢ (2^{nd} (X) \in TEndo (K) (W) \land 2^{nd} (Y) \in TEndo (K) (W) \land (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)) \to (2^{nd} (X) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = 2^{nd} (X) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \circ 2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
38	26 28 35 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (2^{nd} (X) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = 2^{nd} (X) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \circ 2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
39	3 10 11 4 21 36 22	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h)))$
40	39	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h)))$
41	40	oveqd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y) = 2^{nd} (X) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) 2^{nd} (Y)$
42	41	fveq1d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = (2^{nd} (X) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
43		eqid	$⊢ oc (K) (W) = oc (K) (W)$
44	1 2 3 43 10 5	dicelval1sta	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land X \in I (Q)) \to 1^{st} (X) = 2^{nd} (X) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
45	44	3adant3r	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 1^{st} (X) = 2^{nd} (X) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
46	1 2 3 43 10 5	dicelval1sta	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 1^{st} (Y) = 2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
47	46	3adant3l	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 1^{st} (Y) = 2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
48	45 47	coeq12d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 1^{st} (X) \circ 1^{st} (Y) = 2^{nd} (X) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \circ 2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
49	38 42 48	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 1^{st} (X) \circ 1^{st} (Y) = (2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
50	3 10 11 36	tendoplcl	$⊢ ((K \in HL \land W \in H) \land 2^{nd} (X) \in TEndo (K) (W) \land 2^{nd} (Y) \in TEndo (K) (W)) \to 2^{nd} (X) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) 2^{nd} (Y) \in TEndo (K) (W)$
51	7 26 28 50	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 2^{nd} (X) (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (h \in LTrn (K) (W) ⟼ s (h) \circ t (h))) 2^{nd} (Y) \in TEndo (K) (W)$
52	41 51	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y) \in TEndo (K) (W)$
53		fvex	$⊢ 1^{st} (X) \in V$
54		fvex	$⊢ 1^{st} (Y) \in V$
55	53 54	coex	$⊢ 1^{st} (X) \circ 1^{st} (Y) \in V$
56		ovex	$⊢ 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y) \in V$
57	1 2 3 43 10 11 5 55 56	dicopelval	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨1^{st} (X) \circ 1^{st} (Y), 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)⟩ \in I (Q) \leftrightarrow (1^{st} (X) \circ 1^{st} (Y) = (2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y) \in TEndo (K) (W)))$
58	57	3adant3	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to (⟨1^{st} (X) \circ 1^{st} (Y), 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)⟩ \in I (Q) \leftrightarrow (1^{st} (X) \circ 1^{st} (Y) = (2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y) \in TEndo (K) (W)))$
59	49 52 58	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to ⟨1^{st} (X) \circ 1^{st} (Y), 2^{nd} (X) +_{Scalar (U)} 2^{nd} (Y)⟩ \in I (Q)$
60	24 59	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in I (Q) \land Y \in I (Q))) \to X \underset{˙}{+} Y \in I (Q)$

Metamath Proof Explorer

Theorem dicvaddcl

Proof