Metamath Proof Explorer

Theorem sumdmdlem2

Description: Lemma for sumdmdi . (Contributed by NM, 23-Dec-2004) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ⊢ 𝐴 ∈ Cℋ
sumdmdi.2 ⊢ 𝐵 ∈ Cℋ
Assertion sumdmdlem2 ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sumdmdi.1 ⊢ 𝐴 ∈ Cℋ
2 sumdmdi.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
4 3 cheli ⊢ ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑦 ∈ ℋ )
5 spansnsh ⊢ ( 𝑦 ∈ ℋ → ( span ‘ { 𝑦 } ) ∈ Sℋ )
6 2 chshii ⊢ 𝐵 ∈ Sℋ
7 shsub2 ⊢ ( ( ( span ‘ { 𝑦 } ) ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( span ‘ { 𝑦 } ) ⊆ ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) )
8 5 6 7 sylancl ⊢ ( 𝑦 ∈ ℋ → ( span ‘ { 𝑦 } ) ⊆ ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) )
9 spansnid ⊢ ( 𝑦 ∈ ℋ → 𝑦 ∈ ( span ‘ { 𝑦 } ) )
10 8 9 sseldd ⊢ ( 𝑦 ∈ ℋ → 𝑦 ∈ ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) )
11 10 ad2antrl ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → 𝑦 ∈ ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) )
12 elin ⊢ ( 𝑦 ∈ ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑦 ∈ ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∧ 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) )
13 df-ne ⊢ ( 𝑦 ≠ 0ℎ ↔ ¬ 𝑦 = 0ℎ )
14 spansna ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑦 ≠ 0ℎ ) → ( span ‘ { 𝑦 } ) ∈ HAtoms )
15 13 14 sylan2br ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 = 0ℎ ) → ( span ‘ { 𝑦 } ) ∈ HAtoms )
16 oveq1 ⊢ ( 𝑥 = ( span ‘ { 𝑦 } ) → ( 𝑥 ∨ℋ 𝐵 ) = ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) )
17 16 ineq1d ⊢ ( 𝑥 = ( span ‘ { 𝑦 } ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
18 16 ineq1d ⊢ ( 𝑥 = ( span ‘ { 𝑦 } ) → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) )
19 18 oveq1d ⊢ ( 𝑥 = ( span ‘ { 𝑦 } ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
20 17 19 sseq12d ⊢ ( 𝑥 = ( span ‘ { 𝑦 } ) → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
21 20 rspcv ⊢ ( ( span ‘ { 𝑦 } ) ∈ HAtoms → ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
22 15 21 syl ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 = 0ℎ ) → ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
23 spansnj ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ ℋ ) → ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) = ( 𝐵 ∨ℋ ( span ‘ { 𝑦 } ) ) )
24 spansnch ⊢ ( 𝑦 ∈ ℋ → ( span ‘ { 𝑦 } ) ∈ Cℋ )
25 chjcom ⊢ ( ( 𝐵 ∈ Cℋ ∧ ( span ‘ { 𝑦 } ) ∈ Cℋ ) → ( 𝐵 ∨ℋ ( span ‘ { 𝑦 } ) ) = ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) )
26 24 25 sylan2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ ℋ ) → ( 𝐵 ∨ℋ ( span ‘ { 𝑦 } ) ) = ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) )
27 23 26 eqtrd ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑦 ∈ ℋ ) → ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) = ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) )
28 2 27 mpan ⊢ ( 𝑦 ∈ ℋ → ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) = ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) )
29 28 ineq1d ⊢ ( 𝑦 ∈ ℋ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
30 28 ineq1d ⊢ ( 𝑦 ∈ ℋ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) = ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) )
31 30 oveq1d ⊢ ( 𝑦 ∈ ℋ → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
32 29 31 sseq12d ⊢ ( 𝑦 ∈ ℋ → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
33 32 adantr ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 = 0ℎ ) → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( ( span ‘ { 𝑦 } ) ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
34 22 33 sylibrd ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 = 0ℎ ) → ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
35 34 com12 ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 = 0ℎ ) → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
36 35 expdimp ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ 𝑦 ∈ ℋ ) → ( ¬ 𝑦 = 0ℎ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
37 ssid ⊢ 𝐵 ⊆ 𝐵
38 sneq ⊢ ( 𝑦 = 0ℎ → { 𝑦 } = { 0ℎ } )
39 38 fveq2d ⊢ ( 𝑦 = 0ℎ → ( span ‘ { 𝑦 } ) = ( span ‘ { 0ℎ } ) )
40 spansn0 ⊢ ( span ‘ { 0ℎ } ) = 0ℋ
41 39 40 eqtrdi ⊢ ( 𝑦 = 0ℎ → ( span ‘ { 𝑦 } ) = 0ℋ )
42 41 oveq2d ⊢ ( 𝑦 = 0ℎ → ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) = ( 𝐵 +ℋ 0ℋ ) )
43 6 shs0i ⊢ ( 𝐵 +ℋ 0ℋ ) = 𝐵
44 42 43 eqtrdi ⊢ ( 𝑦 = 0ℎ → ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) = 𝐵 )
45 44 ineq1d ⊢ ( 𝑦 = 0ℎ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
46 inss1 ⊢ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐵
47 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
48 37 47 ssini ⊢ 𝐵 ⊆ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
49 46 48 eqssi ⊢ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐵
50 45 49 eqtrdi ⊢ ( 𝑦 = 0ℎ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐵 )
51 44 ineq1d ⊢ ( 𝑦 = 0ℎ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
52 51 oveq1d ⊢ ( 𝑦 = 0ℎ → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
53 2 1 chincli ⊢ ( 𝐵 ∩ 𝐴 ) ∈ Cℋ
54 53 2 chjcomi ⊢ ( ( 𝐵 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ ( 𝐵 ∩ 𝐴 ) )
55 2 1 chabs1i ⊢ ( 𝐵 ∨ℋ ( 𝐵 ∩ 𝐴 ) ) = 𝐵
56 54 55 eqtri ⊢ ( ( 𝐵 ∩ 𝐴 ) ∨ℋ 𝐵 ) = 𝐵
57 52 56 eqtrdi ⊢ ( 𝑦 = 0ℎ → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = 𝐵 )
58 50 57 sseq12d ⊢ ( 𝑦 = 0ℎ → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ 𝐵 ⊆ 𝐵 ) )
59 37 58 mpbiri ⊢ ( 𝑦 = 0ℎ → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
60 36 59 pm2.61d2 ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
61 60 adantrr ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
62 1 2 sumdmdlem ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
63 62 oveq1d ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
64 63 56 eqtrdi ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = 𝐵 )
65 1 chshii ⊢ 𝐴 ∈ Sℋ
66 6 65 shsub2i ⊢ 𝐵 ⊆ ( 𝐴 +ℋ 𝐵 )
67 64 66 eqsstrdi ⊢ ( ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
68 67 adantl ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → ( ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
69 61 68 sstrd ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
70 69 sseld ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → ( 𝑦 ∈ ( ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
71 12 70 syl5bir ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → ( ( 𝑦 ∈ ( 𝐵 +ℋ ( span ‘ { 𝑦 } ) ) ∧ 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
72 11 71 mpand ⊢ ( ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ∧ ( 𝑦 ∈ ℋ ∧ ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
73 72 exp32 ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝑦 ∈ ℋ → ( ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) ) )
74 73 com34 ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝑦 ∈ ℋ → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → ( ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) ) )
75 pm2.18 ⊢ ( ( ¬ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) )
76 74 75 syl8 ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝑦 ∈ ℋ → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) )
77 4 76 syl5 ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) )
78 77 pm2.43d ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
79 78 ssrdv ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
80 1 2 chsleji ⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
81 79 80 jctil ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
82 eqss ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ↔ ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
83 81 82 sylibr ⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )