dih2dimbALTN

Description: Extend dia2dim to isomorphism H. (This version combines dib2dim and dih2dimb for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dih2dimb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dih2dimb.j	$⊢ \underset{˙}{\lor} = join (K)$
	dih2dimb.a	$⊢ A = Atoms (K)$
	dih2dimb.h	$⊢ H = LHyp (K)$
	dih2dimb.u	$⊢ U = DVecH (K) (W)$
	dih2dimb.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dih2dimb.i	$⊢ I = DIsoH (K) (W)$
	dih2dimb.k	$⊢ φ \to (K \in HL \land W \in H)$
	dih2dimb.p	$⊢ φ \to (P \in A \land P \underset{˙}{\leq} W)$
	dih2dimb.q	$⊢ φ \to (Q \in A \land Q \underset{˙}{\leq} W)$
Assertion	dih2dimbALTN	$⊢ φ \to I (P \underset{˙}{\lor} Q) \subseteq I (P) \underset{˙}{\oplus} I (Q)$

Proof

Step	Hyp	Ref	Expression
1		dih2dimb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dih2dimb.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dih2dimb.a	$⊢ A = Atoms (K)$
4		dih2dimb.h	$⊢ H = LHyp (K)$
5		dih2dimb.u	$⊢ U = DVecH (K) (W)$
6		dih2dimb.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
7		dih2dimb.i	$⊢ I = DIsoH (K) (W)$
8		dih2dimb.k	$⊢ φ \to (K \in HL \land W \in H)$
9		dih2dimb.p	$⊢ φ \to (P \in A \land P \underset{˙}{\leq} W)$
10		dih2dimb.q	$⊢ φ \to (Q \in A \land Q \underset{˙}{\leq} W)$
11		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
12	4 11	dibvalrel	$⊢ (K \in HL \land W \in H) \to Rel DIsoB (K) (W) (P \underset{˙}{\lor} Q)$
13	8 12	syl	$⊢ φ \to Rel DIsoB (K) (W) (P \underset{˙}{\lor} Q)$
14		eqid	$⊢ DVecA (K) (W) = DVecA (K) (W)$
15		eqid	$⊢ LSSum (DVecA (K) (W)) = LSSum (DVecA (K) (W))$
16		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
17	1 2 3 4 14 15 16 8 9 10	dia2dim	$⊢ φ \to DIsoA (K) (W) (P \underset{˙}{\lor} Q) \subseteq DIsoA (K) (W) (P) LSSum (DVecA (K) (W)) DIsoA (K) (W) (Q)$
18	17	sseld	$⊢ φ \to (f \in DIsoA (K) (W) (P \underset{˙}{\lor} Q) \to f \in (DIsoA (K) (W) (P) LSSum (DVecA (K) (W)) DIsoA (K) (W) (Q)))$
19	18	anim1d	$⊢ φ \to ((f \in DIsoA (K) (W) (P \underset{˙}{\lor} Q) \land s = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})) \to (f \in (DIsoA (K) (W) (P) LSSum (DVecA (K) (W)) DIsoA (K) (W) (Q)) \land s = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
20	8	simpld	$⊢ φ \to K \in HL$
21	9	simpld	$⊢ φ \to P \in A$
22	10	simpld	$⊢ φ \to Q \in A$
23		eqid	$⊢ {Base}_{K} = {Base}_{K}$
24	23 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
25	20 21 22 24	syl3anc	$⊢ φ \to P \underset{˙}{\lor} Q \in {Base}_{K}$
26	9	simprd	$⊢ φ \to P \underset{˙}{\leq} W$
27	10	simprd	$⊢ φ \to Q \underset{˙}{\leq} W$
28		hllat	$⊢ K \in HL \to K \in Lat$
29	20 28	syl	$⊢ φ \to K \in Lat$
30	23 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
31	21 30	syl	$⊢ φ \to P \in {Base}_{K}$
32	23 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
33	22 32	syl	$⊢ φ \to Q \in {Base}_{K}$
34	8	simprd	$⊢ φ \to W \in H$
35	23 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
36	34 35	syl	$⊢ φ \to W \in {Base}_{K}$
37	23 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\leq} W \land Q \underset{˙}{\leq} W) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W)$
38	29 31 33 36 37	syl13anc	$⊢ φ \to ((P \underset{˙}{\leq} W \land Q \underset{˙}{\leq} W) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W)$
39	26 27 38	mpbi2and	$⊢ φ \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W$
40		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
41		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
42	23 1 4 40 41 16 11	dibopelval2	$⊢ ((K \in HL \land W \in H) \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in DIsoB (K) (W) (P \underset{˙}{\lor} Q) \leftrightarrow (f \in DIsoA (K) (W) (P \underset{˙}{\lor} Q) \land s = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
43	8 25 39 42	syl12anc	$⊢ φ \to (⟨f, s⟩ \in DIsoB (K) (W) (P \underset{˙}{\lor} Q) \leftrightarrow (f \in DIsoA (K) (W) (P \underset{˙}{\lor} Q) \land s = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
44	31 26	jca	$⊢ φ \to (P \in {Base}_{K} \land P \underset{˙}{\leq} W)$
45	33 27	jca	$⊢ φ \to (Q \in {Base}_{K} \land Q \underset{˙}{\leq} W)$
46	23 1 4 40 41 14 5 15 6 16 11 8 44 45	diblsmopel	$⊢ φ \to (⟨f, s⟩ \in (DIsoB (K) (W) (P) \underset{˙}{\oplus} DIsoB (K) (W) (Q)) \leftrightarrow (f \in (DIsoA (K) (W) (P) LSSum (DVecA (K) (W)) DIsoA (K) (W) (Q)) \land s = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})))$
47	19 43 46	3imtr4d	$⊢ φ \to (⟨f, s⟩ \in DIsoB (K) (W) (P \underset{˙}{\lor} Q) \to ⟨f, s⟩ \in (DIsoB (K) (W) (P) \underset{˙}{\oplus} DIsoB (K) (W) (Q)))$
48	13 47	relssdv	$⊢ φ \to DIsoB (K) (W) (P \underset{˙}{\lor} Q) \subseteq DIsoB (K) (W) (P) \underset{˙}{\oplus} DIsoB (K) (W) (Q)$
49	23 1 4 7 11	dihvalb	$⊢ ((K \in HL \land W \in H) \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W)) \to I (P \underset{˙}{\lor} Q) = DIsoB (K) (W) (P \underset{˙}{\lor} Q)$
50	8 25 39 49	syl12anc	$⊢ φ \to I (P \underset{˙}{\lor} Q) = DIsoB (K) (W) (P \underset{˙}{\lor} Q)$
51	23 1 4 7 11	dihvalb	$⊢ ((K \in HL \land W \in H) \land (P \in {Base}_{K} \land P \underset{˙}{\leq} W)) \to I (P) = DIsoB (K) (W) (P)$
52	8 31 26 51	syl12anc	$⊢ φ \to I (P) = DIsoB (K) (W) (P)$
53	23 1 4 7 11	dihvalb	$⊢ ((K \in HL \land W \in H) \land (Q \in {Base}_{K} \land Q \underset{˙}{\leq} W)) \to I (Q) = DIsoB (K) (W) (Q)$
54	8 33 27 53	syl12anc	$⊢ φ \to I (Q) = DIsoB (K) (W) (Q)$
55	52 54	oveq12d	$⊢ φ \to I (P) \underset{˙}{\oplus} I (Q) = DIsoB (K) (W) (P) \underset{˙}{\oplus} DIsoB (K) (W) (Q)$
56	48 50 55	3sstr4d	$⊢ φ \to I (P \underset{˙}{\lor} Q) \subseteq I (P) \underset{˙}{\oplus} I (Q)$

Metamath Proof Explorer

Theorem dih2dimbALTN

Proof