Metamath Proof Explorer

Theorem shmodsi

Description: The modular law holds for subspace sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 23-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shmod.1 ⊢ 𝐴 ∈ Sℋ
shmod.2 ⊢ 𝐵 ∈ Sℋ
shmod.3 ⊢ 𝐶 ∈ Sℋ
Assertion shmodsi ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 shmod.1 ⊢ 𝐴 ∈ Sℋ
2 shmod.2 ⊢ 𝐵 ∈ Sℋ
3 shmod.3 ⊢ 𝐶 ∈ Sℋ
4 elin ⊢ ( 𝑧 ∈ ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) ↔ ( 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) )
5 1 2 shseli ⊢ ( 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 +ℎ 𝑦 ) )
6 3 sheli ⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ )
7 1 sheli ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
8 2 sheli ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ℋ )
9 hvsubadd ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 ↔ ( 𝑥 +ℎ 𝑦 ) = 𝑧 ) )
10 6 7 8 9 syl3an ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 ↔ ( 𝑥 +ℎ 𝑦 ) = 𝑧 ) )
11 eqcom ⊢ ( ( 𝑥 +ℎ 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝑥 +ℎ 𝑦 ) )
12 10 11 bitrdi ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 ↔ 𝑧 = ( 𝑥 +ℎ 𝑦 ) ) )
13 12 3expb ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 ↔ 𝑧 = ( 𝑥 +ℎ 𝑦 ) ) )
14 3 1 shsvsi ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐶 +ℋ 𝐴 ) )
15 3 1 shscomi ⊢ ( 𝐶 +ℋ 𝐴 ) = ( 𝐴 +ℋ 𝐶 )
16 14 15 eleqtrdi ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐴 +ℋ 𝐶 ) )
17 1 3 shlesb1i ⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐴 +ℋ 𝐶 ) = 𝐶 )
18 17 biimpi ⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 +ℋ 𝐶 ) = 𝐶 )
19 18 eleq2d ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐴 +ℋ 𝐶 ) ↔ ( 𝑧 −ℎ 𝑥 ) ∈ 𝐶 ) )
20 16 19 syl5ib ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 −ℎ 𝑥 ) ∈ 𝐶 ) )
21 eleq1 ⊢ ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 → ( ( 𝑧 −ℎ 𝑥 ) ∈ 𝐶 ↔ 𝑦 ∈ 𝐶 ) )
22 21 biimpd ⊢ ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 → ( ( 𝑧 −ℎ 𝑥 ) ∈ 𝐶 → 𝑦 ∈ 𝐶 ) )
23 20 22 sylan9 ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝑧 −ℎ 𝑥 ) = 𝑦 ) → ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐶 ) )
24 23 anim2d ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝑧 −ℎ 𝑥 ) = 𝑦 ) → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
25 elin ⊢ ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
26 24 25 syl6ibr ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝑧 −ℎ 𝑥 ) = 𝑦 ) → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
27 26 ex ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
28 27 com13 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 → ( 𝐴 ⊆ 𝐶 → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
29 28 ancoms ⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 → ( 𝐴 ⊆ 𝐶 → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
30 29 anasss ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑧 −ℎ 𝑥 ) = 𝑦 → ( 𝐴 ⊆ 𝐶 → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
31 13 30 sylbird ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝐴 ⊆ 𝐶 → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) ) )
32 31 imp ⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝐴 ⊆ 𝐶 → 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) )
33 2 3 shincli ⊢ ( 𝐵 ∩ 𝐶 ) ∈ Sℋ
34 1 33 shsvai ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) )
35 eleq1 ⊢ ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
36 34 35 syl5ibr ⊢ ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
37 36 expd ⊢ ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) )
38 37 com12 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) )
39 38 ad2antrl ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) )
40 39 imp ⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝑦 ∈ ( 𝐵 ∩ 𝐶 ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
41 32 40 syld ⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝐴 ⊆ 𝐶 → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
42 41 exp31 ⊢ ( 𝑧 ∈ 𝐶 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝐴 ⊆ 𝐶 → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) ) )
43 42 rexlimdvv ⊢ ( 𝑧 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 +ℎ 𝑦 ) → ( 𝐴 ⊆ 𝐶 → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) )
44 5 43 syl5bi ⊢ ( 𝑧 ∈ 𝐶 → ( 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) → ( 𝐴 ⊆ 𝐶 → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) )
45 44 com13 ⊢ ( 𝐴 ⊆ 𝐶 → ( 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) → ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) ) )
46 45 impd ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
47 4 46 syl5bi ⊢ ( 𝐴 ⊆ 𝐶 → ( 𝑧 ∈ ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) → 𝑧 ∈ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) ) )
48 47 ssrdv ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 +ℋ 𝐵 ) ∩ 𝐶 ) ⊆ ( 𝐴 +ℋ ( 𝐵 ∩ 𝐶 ) ) )