Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem mdsymlem8 5783

Description: Lemma for mdsym 5784. Lemma 4(ii) of [Maeda] p. 168.

**Hypotheses**
Ref	Expression
mdsymlem1.1	⊢ A ∈ C_ℋ
mdsymlem1.2	⊢ B ∈ C_ℋ
mdsymlem1.3	⊢ C = (A ∨_ℋ p)

**Assertion**
Ref	Expression
mdsymlem8	⊢ ((¬ A = 0_ℋ ∧ ¬ B = 0_ℋ) → ((⊥ ‘B) M_ℋ (⊥ ‘A) ↔ (⊥ ‘A) M_ℋ (⊥ ‘B)))

Distinct variable group(s): A,p B,p

**Proof of Theorem mdsymlem8**
Step	Hyp	Ref	Expression
1		mdsymlem1.1	. . . . . . 7 ⊢ A ∈ C_ℋ
2		mdsymlem1.2	. . . . . . 7 ⊢ B ∈ C_ℋ
3	1, 2	chjcom 5389	. . . . . 6 ⊢ (A ∨_ℋ B) = (B ∨_ℋ A)
4	3	sseq2i 1525	. . . . 5 ⊢ (p ⊆ (A ∨_ℋ B) ↔ p ⊆ (B ∨_ℋ A))
5		chjcomt 5423	. . . . . . . . . 10 ⊢ ((q ∈ C_ℋ ∧ r ∈ C_ℋ ) → (q ∨_ℋ r) = (r ∨_ℋ q))
6		atelch 5742	. . . . . . . . . 10 ⊢ (q ∈ Atoms → q ∈ C_ℋ )
7		atelch 5742	. . . . . . . . . 10 ⊢ (r ∈ Atoms → r ∈ C_ℋ )
8	5, 6, 7	syl2an 349	. . . . . . . . 9 ⊢ ((q ∈ Atoms ∧ r ∈ Atoms) → (q ∨_ℋ r) = (r ∨_ℋ q))
9	8	sseq2d 1528	. . . . . . . 8 ⊢ ((q ∈ Atoms ∧ r ∈ Atoms) → (p ⊆ (q ∨_ℋ r) ↔ p ⊆ (r ∨_ℋ q)))
10		ancom 333	. . . . . . . . 9 ⊢ ((q ⊆ A ∧ r ⊆ B) ↔ (r ⊆ B ∧ q ⊆ A))
11	10	a1i 7	. . . . . . . 8 ⊢ ((q ∈ Atoms ∧ r ∈ Atoms) → ((q ⊆ A ∧ r ⊆ B) ↔ (r ⊆ B ∧ q ⊆ A)))
12	9, 11	anbi12d 476	. . . . . . 7 ⊢ ((q ∈ Atoms ∧ r ∈ Atoms) → ((p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)) ↔ (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A))))
13	12	bi2rexa 1230	. . . . . 6 ⊢ (∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)) ↔ ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)))
14		rexcom 1313	. . . . . 6 ⊢ (∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)) ↔ ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)))
15	13, 14	bitr 151	. . . . 5 ⊢ (∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)) ↔ ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)))
16	4, 15	imbi12i 163	. . . 4 ⊢ ((p ⊆ (A ∨_ℋ B) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B))) ↔ (p ⊆ (B ∨_ℋ A) → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A))))
17	16	biral 1223	. . 3 ⊢ (∀p ∈ Atoms (p ⊆ (A ∨_ℋ B) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B))) ↔ ∀p ∈ Atoms (p ⊆ (B ∨_ℋ A) → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A))))
18	17	a1i 7	. 2 ⊢ ((¬ A = 0_ℋ ∧ ¬ B = 0_ℋ) → (∀p ∈ Atoms (p ⊆ (A ∨_ℋ B) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B))) ↔ ∀p ∈ Atoms (p ⊆ (B ∨_ℋ A) → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)))))
19		mdsymlem1.3	. . 3 ⊢ C = (A ∨_ℋ p)
20	1, 2, 19	mdsymlem7 5782	. 2 ⊢ ((¬ A = 0_ℋ ∧ ¬ B = 0_ℋ) → ((⊥ ‘B) M_ℋ (⊥ ‘A) ↔ ∀p ∈ Atoms (p ⊆ (A ∨_ℋ B) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨_ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)))))
21		cleqid 1102	. . . 4 ⊢ (B ∨_ℋ p) = (B ∨_ℋ p)
22	2, 1, 21	mdsymlem7 5782	. . 3 ⊢ ((¬ B = 0_ℋ ∧ ¬ A = 0_ℋ) → ((⊥ ‘A) M_ℋ (⊥ ‘B) ↔ ∀p ∈ Atoms (p ⊆ (B ∨_ℋ A) → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)))))
23	22	ancoms 334	. 2 ⊢ ((¬ A = 0_ℋ ∧ ¬ B = 0_ℋ) → ((⊥ ‘A) M_ℋ (⊥ ‘B) ↔ ∀p ∈ Atoms (p ⊆ (B ∨_ℋ A) → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (r ∨_ℋ q) ∧ (r ⊆ B ∧ q ⊆ A)))))
24	18, 20, 23	3bitr4d 424	1 ⊢ ((¬ A = 0_ℋ ∧ ¬ B = 0_ℋ) → ((⊥ ‘B) M_ℋ (⊥ ‘A) ↔ (⊥ ‘A) M_ℋ (⊥ ‘B)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 ⊆ wss 1487 class class class wbr 2054 ‘cfv 2422 (class class class)co 3001 C_ℋ cch 4968 ⊥cort 4969 ∨_ℋ chj 4972 0_ℋc0h 4974 Atomscat 4980 M_ℋ cmd 4982

This theorem is referenced by: mdsym 5784

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-ac 1080 ax-hilex 4983 ax-hvaddcl 4984 ax-hvcom 4985 ax-hvass 4986 ax-hvzercl 4987 ax-hvaddid 4988 ax-hvmulcl 4989 ax-hvmulid 4991 ax-hvmulass 4992 ax-hvdistr1 4993 ax-hvdistr2 4994 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048 ax-hcompl 5113

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-i 4037 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-4 4464 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676 df-sqr 4728 df-re 4790 df-im 4791 df-cj 4792 df-abs 4793 df-clim 4876 df-hvsub 4996 df-hnorm 5074 df-cauchy 5102 df-hlim 5107 df-sh 5114 df-ch 5127 df-oc 5156 df-ch0 5157 df-pj 5244 df-shsum 5275 df-span 5276 df-chj 5277 df-chsup 5278 df-cv 5712 df-md 5713 df-at 5737

metamath.org