lmiisolem

	Ref	Expression
Hypotheses	ismid.p	$⊢ P = {Base}_{G}$
	ismid.d	$⊢ \underset{˙}{-} = dist (G)$
	ismid.i	$⊢ I = Itv (G)$
	ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
	lmif.l	$⊢ L = {Line}_{𝒢} (G)$
	lmif.d	$⊢ φ \to D \in ran L$
	lmiiso.1	$⊢ φ \to A \in P$
	lmiiso.2	$⊢ φ \to B \in P$
	lmiisolem.s	$⊢ S = {pInv}_{𝒢} (G) (Z)$
	lmiisolem.z	$⊢ Z = (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B))$
Assertion	lmiisolem	$⊢ φ \to M (A) \underset{˙}{-} M (B) = A \underset{˙}{-} B$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$⊢ P = {Base}_{G}$
2		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
3		ismid.i	$⊢ I = Itv (G)$
4		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		lmif.m	$⊢ M = {lInv}_{𝒢} (G) (D)$
7		lmif.l	$⊢ L = {Line}_{𝒢} (G)$
8		lmif.d	$⊢ φ \to D \in ran L$
9		lmiiso.1	$⊢ φ \to A \in P$
10		lmiiso.2	$⊢ φ \to B \in P$
11		lmiisolem.s	$⊢ S = {pInv}_{𝒢} (G) (Z)$
12		lmiisolem.z	$⊢ Z = (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B))$
13	4	adantr	$⊢ (φ \land S (A) = Z) \to G \in 𝒢_{Tarski}$
14	1 2 3 4 5 6 7 8 9	lmicl	$⊢ φ \to M (A) \in P$
15	1 2 3 4 5 9 14	midcl	$⊢ φ \to A {mid}_{𝒢} (G) M (A) \in P$
16	1 2 3 4 5 6 7 8 10	lmicl	$⊢ φ \to M (B) \in P$
17	1 2 3 4 5 10 16	midcl	$⊢ φ \to B {mid}_{𝒢} (G) M (B) \in P$
18	1 2 3 4 5 15 17	midcl	$⊢ φ \to (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) \in P$
19	12 18	eqeltrid	$⊢ φ \to Z \in P$
20	19	adantr	$⊢ (φ \land S (A) = Z) \to Z \in P$
21		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
22	1 2 3 7 21 4 19 11 9	mircl	$⊢ φ \to S (A) \in P$
23	22	adantr	$⊢ (φ \land S (A) = Z) \to S (A) \in P$
24	9	adantr	$⊢ (φ \land S (A) = Z) \to A \in P$
25	1 2 3 7 21 13 20 11 24	mircgr	$⊢ (φ \land S (A) = Z) \to Z \underset{˙}{-} S (A) = Z \underset{˙}{-} A$
26		simpr	$⊢ (φ \land S (A) = Z) \to S (A) = Z$
27	26	eqcomd	$⊢ (φ \land S (A) = Z) \to Z = S (A)$
28	1 2 3 13 20 23 20 24 25 27	tgcgreq	$⊢ (φ \land S (A) = Z) \to Z = A$
29		simpr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)$
30	29	oveq2d	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) = (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B))$
31	12 30	eqtr4id	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to Z = (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A))$
32	4	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to G \in 𝒢_{Tarski}$
33	5	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to G {Dim}_{𝒢} \geq 2$
34	15	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to A {mid}_{𝒢} (G) M (A) \in P$
35	1 2 3 32 33 34 34	midid	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) = A {mid}_{𝒢} (G) M (A)$
36	31 35	eqtrd	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to Z = A {mid}_{𝒢} (G) M (A)$
37		eqidd	$⊢ φ \to M (A) = M (A)$
38	1 2 3 4 5 6 7 8 9 14	islmib	$⊢ φ \to (M (A) = M (A) \leftrightarrow (A {mid}_{𝒢} (G) M (A) \in D \land (D ⟂_{𝒢} (G) (A L M (A)) \lor A = M (A))))$
39	37 38	mpbid	$⊢ φ \to (A {mid}_{𝒢} (G) M (A) \in D \land (D ⟂_{𝒢} (G) (A L M (A)) \lor A = M (A)))$
40	39	simpld	$⊢ φ \to A {mid}_{𝒢} (G) M (A) \in D$
41	40	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to A {mid}_{𝒢} (G) M (A) \in D$
42	36 41	eqeltrd	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = B {mid}_{𝒢} (G) M (B)) \to Z \in D$
43	4	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to G \in 𝒢_{Tarski}$
44	15	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to A {mid}_{𝒢} (G) M (A) \in P$
45	17	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to B {mid}_{𝒢} (G) M (B) \in P$
46	19	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to Z \in P$
47		simpr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)$
48	1 2 3 4 5 15 17	midbtwn	$⊢ φ \to (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) \in ((A {mid}_{𝒢} (G) M (A)) I (B {mid}_{𝒢} (G) M (B)))$
49	12 48	eqeltrid	$⊢ φ \to Z \in ((A {mid}_{𝒢} (G) M (A)) I (B {mid}_{𝒢} (G) M (B)))$
50	49	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to Z \in ((A {mid}_{𝒢} (G) M (A)) I (B {mid}_{𝒢} (G) M (B)))$
51	1 3 7 43 44 45 46 47 50	btwnlng1	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to Z \in ((A {mid}_{𝒢} (G) M (A)) L (B {mid}_{𝒢} (G) M (B)))$
52	8	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to D \in ran L$
53	40	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to A {mid}_{𝒢} (G) M (A) \in D$
54		eqidd	$⊢ φ \to M (B) = M (B)$
55	1 2 3 4 5 6 7 8 10 16	islmib	$⊢ φ \to (M (B) = M (B) \leftrightarrow (B {mid}_{𝒢} (G) M (B) \in D \land (D ⟂_{𝒢} (G) (B L M (B)) \lor B = M (B))))$
56	54 55	mpbid	$⊢ φ \to (B {mid}_{𝒢} (G) M (B) \in D \land (D ⟂_{𝒢} (G) (B L M (B)) \lor B = M (B)))$
57	56	simpld	$⊢ φ \to B {mid}_{𝒢} (G) M (B) \in D$
58	57	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to B {mid}_{𝒢} (G) M (B) \in D$
59	1 3 7 43 44 45 47 47 52 53 58	tglinethru	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to D = (A {mid}_{𝒢} (G) M (A)) L (B {mid}_{𝒢} (G) M (B))$
60	51 59	eleqtrrd	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) \neq B {mid}_{𝒢} (G) M (B)) \to Z \in D$
61	42 60	pm2.61dane	$⊢ φ \to Z \in D$
62	61	adantr	$⊢ (φ \land S (A) = Z) \to Z \in D$
63	28 62	eqeltrrd	$⊢ (φ \land S (A) = Z) \to A \in D$
64	1 2 3 4 5 6 7 8 9	lmiinv	$⊢ φ \to (M (A) = A \leftrightarrow A \in D)$
65	64	biimpar	$⊢ (φ \land A \in D) \to M (A) = A$
66	63 65	syldan	$⊢ (φ \land S (A) = Z) \to M (A) = A$
67	66 28	eqtr4d	$⊢ (φ \land S (A) = Z) \to M (A) = Z$
68	67	oveq1d	$⊢ (φ \land S (A) = Z) \to M (A) \underset{˙}{-} M (B) = Z \underset{˙}{-} M (B)$
69		eqidd	$⊢ (φ \land B = M (B)) \to Z = Z$
70	4	adantr	$⊢ (φ \land B = M (B)) \to G \in 𝒢_{Tarski}$
71	10	adantr	$⊢ (φ \land B = M (B)) \to B \in P$
72	17	adantr	$⊢ (φ \land B = M (B)) \to B {mid}_{𝒢} (G) M (B) \in P$
73	1 2 3 4 5 10 16	midbtwn	$⊢ φ \to B {mid}_{𝒢} (G) M (B) \in (B I M (B))$
74	73	adantr	$⊢ (φ \land B = M (B)) \to B {mid}_{𝒢} (G) M (B) \in (B I M (B))$
75		simpr	$⊢ (φ \land B = M (B)) \to B = M (B)$
76	75	oveq2d	$⊢ (φ \land B = M (B)) \to B I B = B I M (B)$
77	74 76	eleqtrrd	$⊢ (φ \land B = M (B)) \to B {mid}_{𝒢} (G) M (B) \in (B I B)$
78	1 2 3 70 71 72 77	axtgbtwnid	$⊢ (φ \land B = M (B)) \to B = B {mid}_{𝒢} (G) M (B)$
79		eqidd	$⊢ (φ \land B = M (B)) \to B = B$
80	69 78 79	s3eqd	$⊢ (φ \land B = M (B)) \to ⟨“ Z B B ”⟩ = ⟨“ Z (B {mid}_{𝒢} (G) M (B)) B ”⟩$
81	1 2 3 7 21 4 19 10 10	ragtrivb	$⊢ φ \to ⟨“ Z B B ”⟩ \in ∟_{𝒢} (G)$
82	81	adantr	$⊢ (φ \land B = M (B)) \to ⟨“ Z B B ”⟩ \in ∟_{𝒢} (G)$
83	80 82	eqeltrrd	$⊢ (φ \land B = M (B)) \to ⟨“ Z (B {mid}_{𝒢} (G) M (B)) B ”⟩ \in ∟_{𝒢} (G)$
84	4	adantr	$⊢ (φ \land B \neq M (B)) \to G \in 𝒢_{Tarski}$
85	61	adantr	$⊢ (φ \land B \neq M (B)) \to Z \in D$
86	57	adantr	$⊢ (φ \land B \neq M (B)) \to B {mid}_{𝒢} (G) M (B) \in D$
87	10	adantr	$⊢ (φ \land B \neq M (B)) \to B \in P$
88		df-ne	$⊢ B \neq M (B) \leftrightarrow \neg B = M (B)$
89	56	simprd	$⊢ φ \to (D ⟂_{𝒢} (G) (B L M (B)) \lor B = M (B))$
90	89	orcomd	$⊢ φ \to (B = M (B) \lor D ⟂_{𝒢} (G) (B L M (B)))$
91	90	orcanai	$⊢ (φ \land \neg B = M (B)) \to D ⟂_{𝒢} (G) (B L M (B))$
92	88 91	sylan2b	$⊢ (φ \land B \neq M (B)) \to D ⟂_{𝒢} (G) (B L M (B))$
93	16	adantr	$⊢ (φ \land B \neq M (B)) \to M (B) \in P$
94		simpr	$⊢ (φ \land B \neq M (B)) \to B \neq M (B)$
95	17	adantr	$⊢ (φ \land B \neq M (B)) \to B {mid}_{𝒢} (G) M (B) \in P$
96	4	adantr	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to G \in 𝒢_{Tarski}$
97	10	adantr	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to B \in P$
98	16	adantr	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to M (B) \in P$
99	5	adantr	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to G {Dim}_{𝒢} \geq 2$
100		simpr	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to B {mid}_{𝒢} (G) M (B) = B$
101	1 2 3 96 99 97 98 100	midcgr	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to B \underset{˙}{-} B = B \underset{˙}{-} M (B)$
102	101	eqcomd	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to B \underset{˙}{-} M (B) = B \underset{˙}{-} B$
103	1 2 3 96 97 98 97 102	axtgcgrid	$⊢ (φ \land B {mid}_{𝒢} (G) M (B) = B) \to B = M (B)$
104	103	ex	$⊢ φ \to (B {mid}_{𝒢} (G) M (B) = B \to B = M (B))$
105	104	necon3d	$⊢ φ \to (B \neq M (B) \to B {mid}_{𝒢} (G) M (B) \neq B)$
106	105	imp	$⊢ (φ \land B \neq M (B)) \to B {mid}_{𝒢} (G) M (B) \neq B$
107	73	adantr	$⊢ (φ \land B \neq M (B)) \to B {mid}_{𝒢} (G) M (B) \in (B I M (B))$
108	1 3 7 84 87 93 95 94 107	btwnlng1	$⊢ (φ \land B \neq M (B)) \to B {mid}_{𝒢} (G) M (B) \in (B L M (B))$
109	1 3 7 84 87 93 94 95 106 108	tglineelsb2	$⊢ (φ \land B \neq M (B)) \to B L M (B) = B L (B {mid}_{𝒢} (G) M (B))$
110	1 3 7 84 95 87 106	tglinecom	$⊢ (φ \land B \neq M (B)) \to (B {mid}_{𝒢} (G) M (B)) L B = B L (B {mid}_{𝒢} (G) M (B))$
111	109 110	eqtr4d	$⊢ (φ \land B \neq M (B)) \to B L M (B) = (B {mid}_{𝒢} (G) M (B)) L B$
112	92 111	breqtrd	$⊢ (φ \land B \neq M (B)) \to D ⟂_{𝒢} (G) ((B {mid}_{𝒢} (G) M (B)) L B)$
113	1 2 3 7 84 85 86 87 112	perpdrag	$⊢ (φ \land B \neq M (B)) \to ⟨“ Z (B {mid}_{𝒢} (G) M (B)) B ”⟩ \in ∟_{𝒢} (G)$
114	83 113	pm2.61dane	$⊢ φ \to ⟨“ Z (B {mid}_{𝒢} (G) M (B)) B ”⟩ \in ∟_{𝒢} (G)$
115	1 2 3 7 21 4 19 17 10	israg	$⊢ φ \to (⟨“ Z (B {mid}_{𝒢} (G) M (B)) B ”⟩ \in ∟_{𝒢} (G) \leftrightarrow Z \underset{˙}{-} B = Z \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B))$
116	114 115	mpbid	$⊢ φ \to Z \underset{˙}{-} B = Z \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B)$
117		eqidd	$⊢ φ \to B {mid}_{𝒢} (G) M (B) = B {mid}_{𝒢} (G) M (B)$
118	1 2 3 4 5 10 16 21 17	ismidb	$⊢ φ \to (M (B) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B) \leftrightarrow B {mid}_{𝒢} (G) M (B) = B {mid}_{𝒢} (G) M (B))$
119	117 118	mpbird	$⊢ φ \to M (B) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B)$
120	119	oveq2d	$⊢ φ \to Z \underset{˙}{-} M (B) = Z \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B)$
121	116 120	eqtr4d	$⊢ φ \to Z \underset{˙}{-} B = Z \underset{˙}{-} M (B)$
122	121	adantr	$⊢ (φ \land S (A) = Z) \to Z \underset{˙}{-} B = Z \underset{˙}{-} M (B)$
123	28	oveq1d	$⊢ (φ \land S (A) = Z) \to Z \underset{˙}{-} B = A \underset{˙}{-} B$
124	68 122 123	3eqtr2d	$⊢ (φ \land S (A) = Z) \to M (A) \underset{˙}{-} M (B) = A \underset{˙}{-} B$
125	4	adantr	$⊢ (φ \land S (A) \neq Z) \to G \in 𝒢_{Tarski}$
126	22	adantr	$⊢ (φ \land S (A) \neq Z) \to S (A) \in P$
127	19	adantr	$⊢ (φ \land S (A) \neq Z) \to Z \in P$
128	9	adantr	$⊢ (φ \land S (A) \neq Z) \to A \in P$
129	1 2 3 7 21 4 19 11 14	mircl	$⊢ φ \to S (M (A)) \in P$
130	129	adantr	$⊢ (φ \land S (A) \neq Z) \to S (M (A)) \in P$
131	14	adantr	$⊢ (φ \land S (A) \neq Z) \to M (A) \in P$
132	10	adantr	$⊢ (φ \land S (A) \neq Z) \to B \in P$
133	16	adantr	$⊢ (φ \land S (A) \neq Z) \to M (B) \in P$
134		simpr	$⊢ (φ \land S (A) \neq Z) \to S (A) \neq Z$
135	1 2 3 7 21 125 127 11 128	mirbtwn	$⊢ (φ \land S (A) \neq Z) \to Z \in (S (A) I A)$
136	1 2 3 7 21 125 127 11 131	mirbtwn	$⊢ (φ \land S (A) \neq Z) \to Z \in (S (M (A)) I M (A))$
137		eqidd	$⊢ (φ \land A = M (A)) \to Z = Z$
138	4	adantr	$⊢ (φ \land A = M (A)) \to G \in 𝒢_{Tarski}$
139	9	adantr	$⊢ (φ \land A = M (A)) \to A \in P$
140	15	adantr	$⊢ (φ \land A = M (A)) \to A {mid}_{𝒢} (G) M (A) \in P$
141	1 2 3 4 5 9 14	midbtwn	$⊢ φ \to A {mid}_{𝒢} (G) M (A) \in (A I M (A))$
142	141	adantr	$⊢ (φ \land A = M (A)) \to A {mid}_{𝒢} (G) M (A) \in (A I M (A))$
143		simpr	$⊢ (φ \land A = M (A)) \to A = M (A)$
144	143	oveq2d	$⊢ (φ \land A = M (A)) \to A I A = A I M (A)$
145	142 144	eleqtrrd	$⊢ (φ \land A = M (A)) \to A {mid}_{𝒢} (G) M (A) \in (A I A)$
146	1 2 3 138 139 140 145	axtgbtwnid	$⊢ (φ \land A = M (A)) \to A = A {mid}_{𝒢} (G) M (A)$
147		eqidd	$⊢ (φ \land A = M (A)) \to A = A$
148	137 146 147	s3eqd	$⊢ (φ \land A = M (A)) \to ⟨“ Z A A ”⟩ = ⟨“ Z (A {mid}_{𝒢} (G) M (A)) A ”⟩$
149	1 2 3 7 21 4 19 9 9	ragtrivb	$⊢ φ \to ⟨“ Z A A ”⟩ \in ∟_{𝒢} (G)$
150	149	adantr	$⊢ (φ \land A = M (A)) \to ⟨“ Z A A ”⟩ \in ∟_{𝒢} (G)$
151	148 150	eqeltrrd	$⊢ (φ \land A = M (A)) \to ⟨“ Z (A {mid}_{𝒢} (G) M (A)) A ”⟩ \in ∟_{𝒢} (G)$
152	4	adantr	$⊢ (φ \land A \neq M (A)) \to G \in 𝒢_{Tarski}$
153	61	adantr	$⊢ (φ \land A \neq M (A)) \to Z \in D$
154	40	adantr	$⊢ (φ \land A \neq M (A)) \to A {mid}_{𝒢} (G) M (A) \in D$
155	9	adantr	$⊢ (φ \land A \neq M (A)) \to A \in P$
156		df-ne	$⊢ A \neq M (A) \leftrightarrow \neg A = M (A)$
157	39	simprd	$⊢ φ \to (D ⟂_{𝒢} (G) (A L M (A)) \lor A = M (A))$
158	157	orcomd	$⊢ φ \to (A = M (A) \lor D ⟂_{𝒢} (G) (A L M (A)))$
159	158	orcanai	$⊢ (φ \land \neg A = M (A)) \to D ⟂_{𝒢} (G) (A L M (A))$
160	156 159	sylan2b	$⊢ (φ \land A \neq M (A)) \to D ⟂_{𝒢} (G) (A L M (A))$
161	14	adantr	$⊢ (φ \land A \neq M (A)) \to M (A) \in P$
162		simpr	$⊢ (φ \land A \neq M (A)) \to A \neq M (A)$
163	15	adantr	$⊢ (φ \land A \neq M (A)) \to A {mid}_{𝒢} (G) M (A) \in P$
164	4	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to G \in 𝒢_{Tarski}$
165	9	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to A \in P$
166	14	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to M (A) \in P$
167	5	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to G {Dim}_{𝒢} \geq 2$
168		simpr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to A {mid}_{𝒢} (G) M (A) = A$
169	1 2 3 164 167 165 166 168	midcgr	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to A \underset{˙}{-} A = A \underset{˙}{-} M (A)$
170	169	eqcomd	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to A \underset{˙}{-} M (A) = A \underset{˙}{-} A$
171	1 2 3 164 165 166 165 170	axtgcgrid	$⊢ (φ \land A {mid}_{𝒢} (G) M (A) = A) \to A = M (A)$
172	171	ex	$⊢ φ \to (A {mid}_{𝒢} (G) M (A) = A \to A = M (A))$
173	172	necon3d	$⊢ φ \to (A \neq M (A) \to A {mid}_{𝒢} (G) M (A) \neq A)$
174	173	imp	$⊢ (φ \land A \neq M (A)) \to A {mid}_{𝒢} (G) M (A) \neq A$
175	141	adantr	$⊢ (φ \land A \neq M (A)) \to A {mid}_{𝒢} (G) M (A) \in (A I M (A))$
176	1 3 7 152 155 161 163 162 175	btwnlng1	$⊢ (φ \land A \neq M (A)) \to A {mid}_{𝒢} (G) M (A) \in (A L M (A))$
177	1 3 7 152 155 161 162 163 174 176	tglineelsb2	$⊢ (φ \land A \neq M (A)) \to A L M (A) = A L (A {mid}_{𝒢} (G) M (A))$
178	1 3 7 152 163 155 174	tglinecom	$⊢ (φ \land A \neq M (A)) \to (A {mid}_{𝒢} (G) M (A)) L A = A L (A {mid}_{𝒢} (G) M (A))$
179	177 178	eqtr4d	$⊢ (φ \land A \neq M (A)) \to A L M (A) = (A {mid}_{𝒢} (G) M (A)) L A$
180	160 179	breqtrd	$⊢ (φ \land A \neq M (A)) \to D ⟂_{𝒢} (G) ((A {mid}_{𝒢} (G) M (A)) L A)$
181	1 2 3 7 152 153 154 155 180	perpdrag	$⊢ (φ \land A \neq M (A)) \to ⟨“ Z (A {mid}_{𝒢} (G) M (A)) A ”⟩ \in ∟_{𝒢} (G)$
182	151 181	pm2.61dane	$⊢ φ \to ⟨“ Z (A {mid}_{𝒢} (G) M (A)) A ”⟩ \in ∟_{𝒢} (G)$
183	1 2 3 7 21 4 19 15 9	israg	$⊢ φ \to (⟨“ Z (A {mid}_{𝒢} (G) M (A)) A ”⟩ \in ∟_{𝒢} (G) \leftrightarrow Z \underset{˙}{-} A = Z \underset{˙}{-} {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) (A))$
184	182 183	mpbid	$⊢ φ \to Z \underset{˙}{-} A = Z \underset{˙}{-} {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) (A)$
185		eqidd	$⊢ φ \to A {mid}_{𝒢} (G) M (A) = A {mid}_{𝒢} (G) M (A)$
186	1 2 3 4 5 9 14 21 15	ismidb	$⊢ φ \to (M (A) = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) (A) \leftrightarrow A {mid}_{𝒢} (G) M (A) = A {mid}_{𝒢} (G) M (A))$
187	185 186	mpbird	$⊢ φ \to M (A) = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) (A)$
188	187	oveq2d	$⊢ φ \to Z \underset{˙}{-} M (A) = Z \underset{˙}{-} {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) M (A)) (A)$
189	184 188	eqtr4d	$⊢ φ \to Z \underset{˙}{-} A = Z \underset{˙}{-} M (A)$
190	1 2 3 7 21 4 19 11 9	mircgr	$⊢ φ \to Z \underset{˙}{-} S (A) = Z \underset{˙}{-} A$
191	1 2 3 7 21 4 19 11 14	mircgr	$⊢ φ \to Z \underset{˙}{-} S (M (A)) = Z \underset{˙}{-} M (A)$
192	189 190 191	3eqtr4d	$⊢ φ \to Z \underset{˙}{-} S (A) = Z \underset{˙}{-} S (M (A))$
193	192	adantr	$⊢ (φ \land S (A) \neq Z) \to Z \underset{˙}{-} S (A) = Z \underset{˙}{-} S (M (A))$
194	1 2 3 125 127 126 127 130 193	tgcgrcomlr	$⊢ (φ \land S (A) \neq Z) \to S (A) \underset{˙}{-} Z = S (M (A)) \underset{˙}{-} Z$
195	189	adantr	$⊢ (φ \land S (A) \neq Z) \to Z \underset{˙}{-} A = Z \underset{˙}{-} M (A)$
196	11	fveq1i	$⊢ S (A {mid}_{𝒢} (G) M (A)) = {pInv}_{𝒢} (G) (Z) (A {mid}_{𝒢} (G) M (A))$
197	1 2 3 4 5 9 14 11 19	mirmid	$⊢ φ \to S (A) {mid}_{𝒢} (G) S (M (A)) = S (A {mid}_{𝒢} (G) M (A))$
198	12	eqcomi	$⊢ (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) = Z$
199	1 2 3 4 5 15 17 21 19	ismidb	$⊢ φ \to (B {mid}_{𝒢} (G) M (B) = {pInv}_{𝒢} (G) (Z) (A {mid}_{𝒢} (G) M (A)) \leftrightarrow (A {mid}_{𝒢} (G) M (A)) {mid}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) = Z)$
200	198 199	mpbiri	$⊢ φ \to B {mid}_{𝒢} (G) M (B) = {pInv}_{𝒢} (G) (Z) (A {mid}_{𝒢} (G) M (A))$
201	196 197 200	3eqtr4a	$⊢ φ \to S (A) {mid}_{𝒢} (G) S (M (A)) = B {mid}_{𝒢} (G) M (B)$
202	1 2 3 4 5 22 129 21 17	ismidb	$⊢ φ \to (S (M (A)) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (S (A)) \leftrightarrow S (A) {mid}_{𝒢} (G) S (M (A)) = B {mid}_{𝒢} (G) M (B))$
203	201 202	mpbird	$⊢ φ \to S (M (A)) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (S (A))$
204	119 203	oveq12d	$⊢ φ \to M (B) \underset{˙}{-} S (M (A)) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (S (A))$
205		eqid	$⊢ {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B))$
206	1 2 3 7 21 4 17 205 10 22	miriso	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (B) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) M (B)) (S (A)) = B \underset{˙}{-} S (A)$
207	204 206	eqtr2d	$⊢ φ \to B \underset{˙}{-} S (A) = M (B) \underset{˙}{-} S (M (A))$
208	207	adantr	$⊢ (φ \land S (A) \neq Z) \to B \underset{˙}{-} S (A) = M (B) \underset{˙}{-} S (M (A))$
209	1 2 3 125 132 126 133 130 208	tgcgrcomlr	$⊢ (φ \land S (A) \neq Z) \to S (A) \underset{˙}{-} B = S (M (A)) \underset{˙}{-} M (B)$
210	121	adantr	$⊢ (φ \land S (A) \neq Z) \to Z \underset{˙}{-} B = Z \underset{˙}{-} M (B)$
211	1 2 3 125 126 127 128 130 127 131 132 133 134 135 136 194 195 209 210	axtg5seg	$⊢ (φ \land S (A) \neq Z) \to A \underset{˙}{-} B = M (A) \underset{˙}{-} M (B)$
212	211	eqcomd	$⊢ (φ \land S (A) \neq Z) \to M (A) \underset{˙}{-} M (B) = A \underset{˙}{-} B$
213	124 212	pm2.61dane	$⊢ φ \to M (A) \underset{˙}{-} M (B) = A \underset{˙}{-} B$

Metamath Proof Explorer

Theorem lmiisolem

Proof