dih2dimb

Description: Extend dib2dim to isomorphism H. (Contributed by NM, 22-Sep-2014)

	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	dih2dimb	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

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	1 2 3 4 5 6 11 8 9 10	dib2dim	⊢ ( 𝜑 → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
13	8	simpld	⊢ ( 𝜑 → 𝐾 ∈ HL )
14	9	simpld	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
15	10	simpld	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17	16 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
18	13 14 15 17	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
19	9	simprd	⊢ ( 𝜑 → 𝑃 ≤ 𝑊 )
20	10	simprd	⊢ ( 𝜑 → 𝑄 ≤ 𝑊 )
21	13	hllatd	⊢ ( 𝜑 → 𝐾 ∈ Lat )
22	16 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23	14 22	syl	⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
24	16 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25	15 24	syl	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
26	8	simprd	⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
27	16 4	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28	26 27	syl	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
29	16 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
30	21 23 25 28 29	syl13anc	⊢ ( 𝜑 → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
31	19 20 30	mpbi2and	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 )
32	16 1 4 7 11	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
33	8 18 31 32	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ∨ 𝑄 ) ) )
34	16 1 4 7 11	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
35	8 23 19 34	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
36	16 1 4 7 11	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
37	8 25 20 36	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
38	35 37	oveq12d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) = ( ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
39	12 33 38	3sstr4d	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑃 ∨ 𝑄 ) ) ⊆ ( ( 𝐼 ‘ 𝑃 ) ⊕ ( 𝐼 ‘ 𝑄 ) ) )

Metamath Proof Explorer

Theorem dih2dimb

Proof