Metamath Proof Explorer

Theorem dihjatcclem3

Description: Lemma for dihjatcc . (Contributed by NM, 28-Sep-2014)

Ref Expression
Hypotheses dihjatcclem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihjatcclem.l ⊢ ≤ = ( le ‘ 𝐾 )
dihjatcclem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihjatcclem.j ⊢ ∨ = ( join ‘ 𝐾 )
dihjatcclem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihjatcclem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihjatcclem.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjatcclem.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihjatcclem.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihjatcclem.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
dihjatcclem.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihjatcclem.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
dihjatcclem.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
dihjatcc.w ⊢ 𝐶 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihjatcc.g ⊢ 𝐺 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑃 )
dihjatcc.dd ⊢ 𝐷 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑄 )
Assertion dihjatcclem3 ( 𝜑 → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 dihjatcclem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihjatcclem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihjatcclem.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihjatcclem.j ⊢ ∨ = ( join ‘ 𝐾 )
5 dihjatcclem.m ⊢ ∧ = ( meet ‘ 𝐾 )
6 dihjatcclem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 dihjatcclem.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 dihjatcclem.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
9 dihjatcclem.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
10 dihjatcclem.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
11 dihjatcclem.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 dihjatcclem.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
13 dihjatcclem.q ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
14 dihjatcc.w ⊢ 𝐶 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
15 dihjatcc.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16 dihjatcc.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
17 dihjatcc.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
18 dihjatcc.g ⊢ 𝐺 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑃 )
19 dihjatcc.dd ⊢ 𝐷 = ( ℩ 𝑑 ∈ 𝑇 ( 𝑑 ‘ 𝐶 ) = 𝑄 )
20 2 6 3 14 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) )
21 11 20 syl ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) )
22 2 6 3 15 18 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
23 11 21 12 22 syl3anc ⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )
24 2 6 3 15 19 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐷 ∈ 𝑇 )
25 11 21 13 24 syl3anc ⊢ ( 𝜑 → 𝐷 ∈ 𝑇 )
26 3 15 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝑇 ) → ◡ 𝐷 ∈ 𝑇 )
27 11 25 26 syl2anc ⊢ ( 𝜑 → ◡ 𝐷 ∈ 𝑇 )
28 3 15 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐷 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 )
29 11 23 27 28 syl3anc ⊢ ( 𝜑 → ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 )
30 2 4 5 6 3 15 16 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐷 ) ∈ 𝑇 ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = ( ( 𝑄 ∨ ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) ) ∧ 𝑊 ) )
31 11 29 13 30 syl3anc ⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = ( ( 𝑄 ∨ ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) ) ∧ 𝑊 ) )
32 13 simpld ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
33 2 6 3 15 ltrncoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ◡ 𝐷 ∈ 𝑇 ) ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) = ( 𝐺 ‘ ( ◡ 𝐷 ‘ 𝑄 ) ) )
34 11 23 27 32 33 syl121anc ⊢ ( 𝜑 → ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) = ( 𝐺 ‘ ( ◡ 𝐷 ‘ 𝑄 ) ) )
35 2 6 3 15 19 ltrniotacnvval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ◡ 𝐷 ‘ 𝑄 ) = 𝐶 )
36 11 21 13 35 syl3anc ⊢ ( 𝜑 → ( ◡ 𝐷 ‘ 𝑄 ) = 𝐶 )
37 36 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( ◡ 𝐷 ‘ 𝑄 ) ) = ( 𝐺 ‘ 𝐶 ) )
38 2 6 3 15 18 ltrniotaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝐶 ) = 𝑃 )
39 11 21 12 38 syl3anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = 𝑃 )
40 37 39 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ ( ◡ 𝐷 ‘ 𝑄 ) ) = 𝑃 )
41 34 40 eqtrd ⊢ ( 𝜑 → ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) = 𝑃 )
42 41 oveq2d ⊢ ( 𝜑 → ( 𝑄 ∨ ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) ) = ( 𝑄 ∨ 𝑃 ) )
43 11 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
44 12 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
45 4 6 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
46 43 44 32 45 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
47 42 46 eqtr4d ⊢ ( 𝜑 → ( 𝑄 ∨ ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) ) = ( 𝑃 ∨ 𝑄 ) )
48 47 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 ∨ ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
49 48 10 eqtr4di ⊢ ( 𝜑 → ( ( 𝑄 ∨ ( ( 𝐺 ∘ ◡ 𝐷 ) ‘ 𝑄 ) ) ∧ 𝑊 ) = 𝑉 )
50 31 49 eqtrd ⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = 𝑉 )