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	⊢ ≤ = ( le ‘ 𝐾 )
	dih2dimb.j	⊢ ∨ = ( join ‘ 𝐾 )
	dih2dimb.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dih2dimb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih2dimb.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih2dimb.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dih2dimb.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih2dimb.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dih2dimb.p	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) )
	dih2dimb.q	⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) )
Assertion	dih2dimbALTN	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dih2dimb.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dih2dimb.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dih2dimb.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		dih2dimb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		dih2dimb.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		dih2dimb.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
7		dih2dimb.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8		dih2dimb.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dih2dimb.p	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) )
10		dih2dimb.q	⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) )
11		eqid	⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
12	4 11	dibvalrel	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
13	8 12	syl	⊢ ( 𝜑 → Rel ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
14		eqid	⊢ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
15		eqid	⊢ ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) )
16		eqid	⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
17	1 2 3 4 14 15 16 8 9 10	dia2dim	⊢ ( 𝜑 → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
18	17	sseld	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) → 𝑓 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ) )
19	18	anim1d	⊢ ( 𝜑 → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) → ( 𝑓 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
20	8	simpld	⊢ ( 𝜑 → 𝐾 ∈ HL )
21	9	simpld	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
22	10	simpld	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24	23 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
25	20 21 22 24	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
26	9	simprd	⊢ ( 𝜑 → 𝑃 ≤ 𝑊 )
27	10	simprd	⊢ ( 𝜑 → 𝑄 ≤ 𝑊 )
28		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
29	20 28	syl	⊢ ( 𝜑 → 𝐾 ∈ Lat )
30	23 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31	21 30	syl	⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32	23 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
33	22 32	syl	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
34	8	simprd	⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
35	23 4	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
36	34 35	syl	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
37	23 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
38	29 31 33 36 37	syl13anc	⊢ ( 𝜑 → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
39	26 27 38	mpbi2and	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 )
40		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
41		eqid	⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
42	23 1 4 40 41 16 11	dibopelval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
43	8 25 39 42	syl12anc	⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
44	31 26	jca	⊢ ( 𝜑 → ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) )
45	33 27	jca	⊢ ( 𝜑 → ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ≤ 𝑊 ) )
46	23 1 4 40 41 14 5 15 6 16 11 8 44 45	diblsmopel	⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ↔ ( 𝑓 ∈ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( LSSum ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∧ 𝑠 = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
47	19 43 46	3imtr4d	⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ) )
48	13 47	relssdv	⊢ ( 𝜑 → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
49	23 1 4 7 11	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
50	8 25 39 49	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
51	23 1 4 7 11	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
52	8 31 26 51	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
53	23 1 4 7 11	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
54	8 33 27 53	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
55	52 54	oveq12d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) = ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
56	48 50 55	3sstr4d	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

Metamath Proof Explorer

Theorem dih2dimbALTN

Proof