dicvscacl

Description: Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	dicvscacl.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicvscacl.a	$⊢ A = Atoms (K)$
	dicvscacl.h	$⊢ H = LHyp (K)$
	dicvscacl.e	$⊢ E = TEndo (K) (W)$
	dicvscacl.u	$⊢ U = DVecH (K) (W)$
	dicvscacl.i	$⊢ I = DIsoC (K) (W)$
	dicvscacl.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
Assertion	dicvscacl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X \underset{˙}{\cdot} Y \in I (Q)$

Proof

Step	Hyp	Ref	Expression
1		dicvscacl.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicvscacl.a	$⊢ A = Atoms (K)$
3		dicvscacl.h	$⊢ H = LHyp (K)$
4		dicvscacl.e	$⊢ E = TEndo (K) (W)$
5		dicvscacl.u	$⊢ U = DVecH (K) (W)$
6		dicvscacl.i	$⊢ I = DIsoC (K) (W)$
7		dicvscacl.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
8		simp1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (K \in HL \land W \in H)$
9		simp3l	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X \in E$
10		eqid	$⊢ {Base}_{U} = {Base}_{U}$
11	1 2 3 6 5 10	dicssdvh	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq {Base}_{U}$
12		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
13	3 12 4 5 10	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = LTrn (K) (W) \times E$
14	13	eqcomd	$⊢ (K \in HL \land W \in H) \to LTrn (K) (W) \times E = {Base}_{U}$
15	14	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to LTrn (K) (W) \times E = {Base}_{U}$
16	11 15	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 E$
17	16	3adant3	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to I (Q) \subseteq LTrn (K) (W) \times E$
18		simp3r	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to Y \in I (Q)$
19	17 18	sseldd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to Y \in (LTrn (K) (W) \times E)$
20	3 12 4 5 7	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (X \in E \land Y \in (LTrn (K) (W) \times E))) \to X \underset{˙}{\cdot} Y = ⟨X (1^{st} (Y)), X \circ 2^{nd} (Y)⟩$
21	8 9 19 20	syl12anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X \underset{˙}{\cdot} Y = ⟨X (1^{st} (Y)), X \circ 2^{nd} (Y)⟩$
22		fvi	$⊢ X \in E \to I (X) = X$
23	9 22	syl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to I (X) = X$
24	23	coeq1d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to I (X) \circ 2^{nd} (Y) = X \circ 2^{nd} (Y)$
25	24	opeq2d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to ⟨X (1^{st} (Y)), I (X) \circ 2^{nd} (Y)⟩ = ⟨X (1^{st} (Y)), X \circ 2^{nd} (Y)⟩$
26	21 25	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X \underset{˙}{\cdot} Y = ⟨X (1^{st} (Y)), I (X) \circ 2^{nd} (Y)⟩$
27		eqid	$⊢ oc (K) (W) = oc (K) (W)$
28	1 2 3 27 12 6	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))$
29	28	3adant3l	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to 1^{st} (Y) = 2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
30	29	fveq2d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X (1^{st} (Y)) = X (2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)))$
31	1 2 3 4 6	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 E$
32	31	3adant3l	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to 2^{nd} (Y) \in E$
33	3 12 4	tendof	$⊢ ((K \in HL \land W \in H) \land 2^{nd} (Y) \in E) \to 2^{nd} (Y) : LTrn (K) (W) ⟶ LTrn (K) (W)$
34	8 32 33	syl2anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to 2^{nd} (Y) : LTrn (K) (W) ⟶ LTrn (K) (W)$
35		eqid	$⊢ oc (K) = oc (K)$
36	1 35 2 3	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
37	36	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
38		simp2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
39		eqid	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) = (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)$
40	1 2 3 12 39	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)$
41	8 37 38 40	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
42		fvco3	$⊢ (2^{nd} (Y) : LTrn (K) (W) ⟶ LTrn (K) (W) \land (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)) \to (X \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = X (2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)))$
43	34 41 42	syl2anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (X \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = X (2^{nd} (Y) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)))$
44	30 43	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X (1^{st} (Y)) = (X \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
45	24	fveq1d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (I (X) \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = (X \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
46	44 45	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X (1^{st} (Y)) = (I (X) \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
47	3 4	tendococl	$⊢ ((K \in HL \land W \in H) \land X \in E \land 2^{nd} (Y) \in E) \to X \circ 2^{nd} (Y) \in E$
48	8 9 32 47	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X \circ 2^{nd} (Y) \in E$
49	24 48	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to I (X) \circ 2^{nd} (Y) \in E$
50		fvex	$⊢ X (1^{st} (Y)) \in V$
51		fvex	$⊢ I (X) \in V$
52		fvex	$⊢ 2^{nd} (Y) \in V$
53	51 52	coex	$⊢ I (X) \circ 2^{nd} (Y) \in V$
54	1 2 3 27 12 4 6 50 53	dicopelval	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨X (1^{st} (Y)), I (X) \circ 2^{nd} (Y)⟩ \in I (Q) \leftrightarrow (X (1^{st} (Y)) = (I (X) \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land I (X) \circ 2^{nd} (Y) \in E))$
55	54	3adant3	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to (⟨X (1^{st} (Y)), I (X) \circ 2^{nd} (Y)⟩ \in I (Q) \leftrightarrow (X (1^{st} (Y)) = (I (X) \circ 2^{nd} (Y)) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land I (X) \circ 2^{nd} (Y) \in E))$
56	46 49 55	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to ⟨X (1^{st} (Y)), I (X) \circ 2^{nd} (Y)⟩ \in I (Q)$
57	26 56	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in E \land Y \in I (Q))) \to X \underset{˙}{\cdot} Y \in I (Q)$

Metamath Proof Explorer

Theorem dicvscacl

Proof